Trail.fs

module Trail

open Microsoft.Z3
open Util
open Stats
open Interval
open GlobalOptions
open BitVector
open Literal
open Clause
open BooleanValuation
open BitVectorValuation
open BoundsValuation
open Database
open TheoryRelation
open Learning

let bumpOrder (db:Ref<Database>) (v:Var) =
    //(!(!db).Variables).varOrder.bump v

    if (!(!db).Theory).isDefined v then
        let tRel = (!(!db).Theory).getThRelation v
        for a in tRel.variableArguments do
            (!(!db).Variables).varOrder.bump a


[<NoComparison>]
type TrailElement =
    | BAssgnmnt of Var*(Literal*Literal)*Interval // Bounds Assignment: BvVar, (previous l expl, previous u expl), previous interval
    | MAssgnmnt of Var*Literal*BitVector // Model Assignment: BvVar, prevBoolExplanation, prevBVset, previous order
    | BoolDecision of Literal
    | Imp of Ref<Clause>*Literal

let isImplication (e:TrailElement) =
    match e with
    | Imp _ -> true
    | _ -> false

let isBoolLiteral (e:TrailElement) =
    match e with
    | BAssgnmnt _
    | MAssgnmnt _ -> false
    | _ -> true

let getBoolLiteral (e:TrailElement) =
    assert(isBoolLiteral e)
    match e with
    | BoolDecision l -> l
    | Imp (c, l) -> l
    | _ -> 0

let getBVVar (e:TrailElement) =
    assert(not (isBoolLiteral e))
    match e with
    | MAssgnmnt (v,_,_) -> v
    | BAssgnmnt (v,_,_) -> v
    | _ -> 0

let updateVarOrder (db:Ref<Database>) (v:Var) =
    (!(!db).Variables).varOrder.suspend v
    if (!(!db).Theory).isDefined v then
        let t = (!(!db).Theory).getThRelation v
        let vars = t.variableArguments
        for bv in vars do
            (!(!db).Variables).varOrder.bump bv

type Trail (sz:int) =
    let mutable size = sz //Allocated space
    let mutable topPtr = 0 //Elements on the trail
    let mutable trailPtr = 0 //Next element to propagate

    let mutable printCount = 0

    let mutable numDecisions = 0
    let mutable numAssignments = 0
    let nullClause = [|0|]

    member r.hasPropagationsPending = trailPtr < topPtr
    member r.getCount = topPtr

    member val trail:TrailElement array = Array.create size (BoolDecision 0) with get, set

    member r.getTrailPtr = trailPtr

    member r.nextPropagation =
        assert(r.hasPropagationsPending) //Safe only if hasPropagationPending returns true
        let l = r.trail.[trailPtr]

        trailPtr <- trailPtr + 1
        l

    member r.lastPropagation =
        assert(trailPtr>0)
        r.trail.[trailPtr - 1]

    member r.propagationDone =
        trailPtr <- trailPtr + 1

    member r.getNumDecisions = numDecisions

    member r.getLiteral(i:int) : Literal =
         if i <= topPtr then
            match r.trail.[i] with
            |BoolDecision l -> l
            |Imp (_,l) -> l
            |_->(0:Literal)
         else
            (0:Literal)

    member r.getExplanation(i:int) : Ref<Clause> =
         if i < topPtr then
            match r.trail.[i] with
            |Imp (e, l) -> e
            |_-> ref nullClause
         else
            ref nullClause

    member r.get(i:int):TrailElement option =
        if i < topPtr then
            Some (r.trail.[i])
        else
            None

    member r.realloc()=
        r.trail <- Array.append r.trail (Array.create size (BoolDecision 0))
        size<- 2*size


    member r. ElementToString (e:TrailElement) =
        match e with
//        | BAssgnmnt (v,_,_) -> "BA" + v.ToString()
//        | MAssgnmnt (v,_,_,_) -> "MA " + v.ToString()
        | BoolDecision l -> "no reason"
        | Imp (e,l) -> (clauseToString (!e)) + " -> " + (l.ToString())
        | _ -> ""


    member private r.pushElement (e:TrailElement) =
        if topPtr >= size then
            r.realloc()
        r.trail.[topPtr]<-e
        topPtr <- topPtr + 1



    member r.Push (bVal:Ref<BooleanValuation>)
                  (bvVal:Ref<BitVectorValuation>)
                  (bounds:Ref<BoundsValuation>)
                  (db:Ref<Database>)
                  (stats:Ref<Statistics>)
                  (e:TrailElement) =
        match e with
        | BoolDecision l ->
            assert ((!bVal).getValueB l = Undefined)
            numDecisions <- numDecisions + 1
            (!bVal).setValueB l r.getNumDecisions |> ignore
            (!stats).Decision()
            updateVarOrder db (lit2var l)
            dbg <| (lazy sprintf "> Decision: %d!" l)
            r.pushElement (BoolDecision l)

        | Imp (cRef, l) ->
            assert ((!bVal).getValueB l = Undefined)
            assert (Array.exists (fun x -> x = 0) !cRef = false)
            assert ((!cRef).[1] = l) // CMW: Required for soundness of Boolean conflict resolution.
            (!bVal).setValueB l r.getNumDecisions |> ignore
            updateVarOrder db (lit2var l)
            (!stats).Implication()
            verbose <| (lazy sprintf " | ==> %d (because of %s)" l (clauseToString !cRef))
            r.pushElement (Imp (cRef, l))
        | MAssgnmnt (v, r, value) ->
           if ((!bvVal).getValue v).isConcreteValue then
              (!(!db).Variables).varOrder.suspend v
        | BAssgnmnt _->
            () //AZ: All the necessary book-keeping has been done beforehand in pushMA,
               //    at this point their role is to trigger visitOccurences in propagation.
        match e with
        | BoolDecision l
        | Imp (_, l) -> r.pushMA l bVal bvVal bounds db stats
        | _ -> None


    member private r.popElement () =
        assert (topPtr > 0)
        //r.dbgPrint ("Pop: " + (trailElem2String r.trail.[topPtr - 1]))
        topPtr <- topPtr - 1

        match r.trail.[topPtr] with
        | BoolDecision _ ->
            numDecisions <- numDecisions - 1
            assert(numDecisions >= 0)
        | MAssgnmnt _ -> ()
        | BAssgnmnt _ -> ()
        | _ -> ()

        if trailPtr > topPtr then
            trailPtr <- topPtr

        r.trail.[topPtr]

    member r.Pop (bVal:Ref<BooleanValuation>)
                 (pAss:Ref<BitVectorValuation>)
                 (bounds:Ref<BoundsValuation>)
                 (db:Ref<Database>) =
        let e = r.popElement ()

        if TRC then
            r.print ("Pop : "+ (r.ElementToString e), pAss, bounds)

        match e with
        | MAssgnmnt (bvVar, oldExplain, oldValue) ->
            assert (bvVar <> 0)
            if oldValue.Length <> 0 then // normal model assignment.
                if ((!pAss).getValue bvVar).isConcreteValue then
                    assert (not oldValue.isConcreteValue)
                    (!(!db).Variables).varOrder.restore bvVar
                (!pAss).mAssignmntsExplanations.[bvVar] <- oldExplain
                (!pAss).setValue bvVar oldValue
        | BAssgnmnt (bvVar, (oldLExplain, oldUExplain), oldBounds) ->
            assert (bvVar <> 0)
            (!bounds).L_explanation.[bvVar] <- oldLExplain
            (!bounds).U_explanation.[bvVar] <- oldUExplain
            (!bounds).set bvVar oldBounds
        | BoolDecision l  ->
            (!bVal).resetValueTAboveCurrentDecisionLevel r.getNumDecisions
            assert (l <> 0)
            (!bVal).resetVal (lit2var l) |> ignore

            (!(!db).Variables).varOrder.restore (lit2var l)
        | Imp (_,l) ->
            assert (l <> 0)
            (!bVal).resetVal (lit2var l) |> ignore
            (!(!db).Variables).varOrder.restore (lit2var l)

    member r.Reset() =  topPtr <- 0
                        trailPtr <- 0

    member r.printClsOrCubeVerbose  (db:Ref<Database>)
                                    (connective:string)
                                    (clause:Ref<Clause>)
                                    =
        let cls_sz = (getSize (!clause)) in
        for j in 1 .. cls_sz do
            let i = (!clause).[j]
            let v = (lit2var i)
            //if j <> 1 then printf "       "
            if (!(!db).Theory).isDefined v  then
                if i < 0 then
                    printf "-"
                else
                    printf " "
                printf "%s" (((!(!db).Theory).getThRelation v).ToString((!db).Numerals))
            else
                printf "%d" i
            printf " (L %02d)" (r.getLevelExpensive v)
            if j < cls_sz then
                printfn " %s " connective
        printfn ""

    member r.printClauseVerbose (db:Ref<Database>) (clause:Ref<Clause>) =
        r.printClsOrCubeVerbose db "\/" clause

    member r.printCubeVerbose (db:Ref<Database>) (cube:Ref<Clause>) =
        r.printClsOrCubeVerbose db "/\\" cube

    member r.print (s:string, bvVal:Ref<BitVectorValuation>, bounds:Ref<BoundsValuation>) =
        if VRB && printCount % 10000 = 0 then
            r.forcePrint (s, bvVal, bounds)
            printCount <- printCount + 1

    member r.forcePrint (s:string, bvVal:Ref<BitVectorValuation>, bounds:Ref<BoundsValuation>) =
        printfn "%s" s
        let mutable lvl = 0
        printfn "==================================================="
        printfn "L %02d ----------------------------------------------" lvl
        for i  in 0 .. topPtr - 1 do
            if i = trailPtr then
                printfn " <---- "
            match r.trail.[i] with
            | MAssgnmnt (var, oe,_) ->
                //lvl <- lvl + 1
                let mutable reason = (!bvVal).mAssignmntsExplanations.[var].ToString()
                let mutable value = ((!bvVal).getValue var).ToString()
                let mutable j = i + 1
                while j < topPtr - 1 do
                    match r.trail.[j] with
                    | MAssgnmnt(v, oldexpl, oldval) when v = var ->
                        value <- oldval.ToString()
                        reason <- oldexpl.ToString()
                        j <- topPtr
                    | _ -> ()
                    j <- j + 1
                printfn " [%s] <-> %d:bv = %s " reason var value
            | BAssgnmnt (var, (oLe, oUe), oldBounds) ->
                let mutable lE = (!bounds).L_explanation.[var].ToString()
                let mutable uE = (!bounds).U_explanation.[var].ToString()
                let mutable intvl = ((!bounds).get var).ToString()
                let mutable j = i + 1
                while j < topPtr - 1 do
                    match r.trail.[j] with
                    | BAssgnmnt(v, (oldL, oldU), oldintvl) when v = var ->
                        intvl <- oldintvl.ToString()
                        lE <- oldL.ToString()
                        uE <- oldU.ToString()
                        j <- topPtr
                    | _ -> ()
                    j <- j + 1
                printfn " [%s /\ %s] <-> %d:bv \in %s " lE uE var intvl
            | BoolDecision l ->
                lvl <- lvl + 1
                printfn "L %02d ----------------------------------------------" lvl
                printfn " * %d" l
            | Imp (e,l) -> printfn " %s -> %s " (clauseToString !e) (l.ToString())
        printfn "==================================================="


    member r.getLevelExpensive (l:Literal) =
        let var = lit2var(l)
        let mutable found = false
        let mutable i = 0
        let mutable lvl = 0

        while (not found && i < r.getCount) do
            match r.trail.[i] with
            | Imp(_, m) -> if var = lit2var(m) then found <- true
            | MAssgnmnt(v, _,_) -> if v = var then found <- true
            | BAssgnmnt(v, _, _) -> if v = var then found <- true
            | BoolDecision m ->
                if var = (lit2var m) then
                     found <- true
                lvl <- lvl + 1
            i <- i + 1
        lvl


    member private r.makeRLEMA (bv:Var, newExpl:Var, newPttrn:BitVector)
                (pAss:Ref<BitVectorValuation>)
                (bounds:Ref<BoundsValuation>)
                (db:Ref<Database>)
                (stats:Ref<Statistics>) =
        let oldPttrn = (!pAss).getValue bv
        let oldExpl = (!pAss).mAssignmntsExplanations.[bv]
        let oldBounds = (!bounds).get bv

        let intrsctn = (BitVector.Intersect newPttrn oldPttrn)
        if intrsctn.isInvalid then
            // Bounds implied model assignment violating a bitpattern
            // CMW: Definitely always cross-theory?
            // AZ: Yes, if a value is invalid within single theory
            //     it wouldn't try to make an assignment.
            let cls = collectLiterals [ Negate newExpl; Negate oldExpl ]
            (None, Some (ref (newClauseFromList cls)))
        elif intrsctn.isConcreteValue && not (oldBounds.Contains intrsctn) then
            // Bit-pattern implied assignment violates bounds
            let violatedBound = if not (BitVector.bvULEQ intrsctn oldBounds.Upper) then
                                    (!bounds).U_explanation.[bv]
                                else
                                    (!bounds).L_explanation.[bv]
            let cls = collectLiterals [ Negate newExpl; Negate oldExpl; Negate violatedBound ]
            (None, Some (ref (newClauseFromList cls)))
        else
            let value_is_a_subset = (BitVector.bvEQ newPttrn intrsctn)

            if value_is_a_subset then
                (!pAss).setValue bv newPttrn
                (!pAss).mAssignmntsExplanations.[bv] <- newExpl
                (!stats).ModelAssignment()
                if newPttrn.isConcreteValue then
                   (!(!db).Variables).varOrder.suspend bv
                trace <| (lazy sprintf  " | ==> %d:bv = %s (because of %d)" bv (newPttrn.ToString()) newExpl)
                (Some (MAssgnmnt (bv, oldExpl, oldPttrn)), None)
            elif not (BitVector.bvEQ newPttrn oldPttrn) then
                // CMW: In this case we may still be able to "learn" something, but it doesn't
                // have the shape of an RLE expression, but a nice regular expression might exist.
                (None, None)
            else
                // This can happen when a Boolean variable gets activated,
                // but the corresponding theory relation and it's variable
                // are already more concrete.
                (None, None)


    member private r.makeBoundsMA (bv:Var, newExpl:Literal, newBounds:Interval)
                                  (bounds:Ref<BoundsValuation>)
                                  (db:Ref<Database>)
                                  (stats:Ref<Statistics>) =
        assert(newExpl <> 0) // CMW: newExpl is the reason for whatever changed in the bounds;
                             // could be lower, could be upper, could be both.

        if newBounds.isEmpty then
            (None, Some (ref (newClauseFromList [Negate newExpl])))
        else
            let newLB, newUB = newBounds.Lower, newBounds.Upper
            let oldBnds = (!bounds).get bv

            // CMW: New bounds are usually tighter than the old ones
            let lower_tighter = (BitVector.bvULT oldBnds.Lower newLB)
            let upper_tighter = (BitVector.bvULT newUB oldBnds.Upper)

            let rel = (!(!db).Theory).getThRelation (lit2var newExpl)
            assert(not (lower_tighter && upper_tighter) || rel.isPAPredicate)

            if lower_tighter || upper_tighter then
                let nL = if lower_tighter then newLB else oldBnds.Lower
                let nU = if upper_tighter then newUB else oldBnds.Upper
                let oldLExpl = (!bounds).L_explanation.[bv]
                let oldUExpl = (!bounds).U_explanation.[bv]

                if BitVector.bvUGT nL nU then
                    //xTheory conflict
                    let mutable cls = []
                    for l in [ oldLExpl; oldUExpl; newExpl ] do
                        let already_in_cls = (List.exists (fun x -> x = (Negate l)) cls)
                        if l <> 0 && not already_in_cls then
                            cls <- (Negate l) :: cls
                    let cc = newClauseFromList cls
                    assert(not (clauseContainsDuplicates cc))
                    (None, Some (ref cc))
                else
                    // These explanations have to be updated here, otherwise the conflict resolution
                    // for the conflict in the previous case will be wrong.
                    if lower_tighter then (!bounds).L_explanation.[bv] <- newExpl
                    if upper_tighter then (!bounds).U_explanation.[bv] <- newExpl
                    let newBnds = Interval(nL, nU)
                    (!bounds).set bv (newBnds)
                    bumpOrder db bv
                    (!stats).ModelAssignment()
                    trace <| (lazy sprintf  " | ==> %d:bv is in %s (because of %d)" bv (newBnds.ToString()) newExpl)
                    (Some (BAssgnmnt (bv, (oldLExpl, oldUExpl), oldBnds)), None)
            else
                // CMW: This can happen, e.g., when we see a new constraint that has weaker bounds
                // than an old one. There's a chance that we run into non-termination issues
                // if we ignore them here (could erroneously learn weak bounds forever).
                (None, None)


    member private r.pushMA (l:Literal)
                            (bVal:Ref<BooleanValuation>)
                            (bvVal:Ref<BitVectorValuation>)
                            (bounds:Ref<BoundsValuation>)
                            (db:Ref<Database>)
                            (stats:Ref<Statistics>) =
        let mutable cnflct = None
        if (!(!db).Theory).isDefined (lit2var l) then
            let rel = (!(!db).Theory).getThRelation (lit2var l)

            // CMW: in a more general framework we would iterate
            // over all theories here and ask each of them for "news".
            // For now, we have only the following two theories.

            // RLEBV Theory hook.
            if rel.isPAPredicate then
                let v = rel.getPAPredicateVariable
                let value = rel.getPAPredicateValue (!db).Numerals

                if isPositive(l) then
                    // Positive PAPredicate
                    let args = (v, rel.getBoolVar, value)
                    let te = r.makeRLEMA args bvVal bounds db stats
                    match te with
                    | (Some(e),None) -> r.pushElement e
                    | (None, Some cRef) ->  cnflct <- Some cRef //xTheory conflict
                    | _ -> ()
                else
                    // Negative PAPredicate
                    if not (value.isConcreteValue) then
                            let oldValue = (!bvVal).getValue v
                            let oldExpl = (!bvVal).getExplanation v

                            let intersection = BitVector.Intersect oldValue value

                            if intersection.isInvalid then
                                assert (oldExpl <> Negate l)

                                // v_eq_old_value := v == oldValue
                                //    oldExpl =>
                                let v_eq_old_value = TheoryRelation(v, Z3_decl_kind.Z3_OP_EQ, (!db).mkNumeral oldValue)
                                let oq = (!(!db).Theory).getThRelationVar v_eq_old_value
                                let v_eq_old_value_lit = match oq with
                                                         | (true, var) -> var
                                                         | (false, _) ->
                                                            let newBool = (!db).mkFreshBooleanVariable ()
                                                            v_eq_old_value.setBoolvar newBool
                                                            (!db).addTheoryRelation v_eq_old_value
                                                            newBool

                                // v_eq_value_lit := v == value
                                // l => v_eq_value_lit
                                let v_eq_value = TheoryRelation(v, Z3_decl_kind.Z3_OP_EQ, (!db).mkNumeral value)
                                let nq = (!(!db).Theory).getThRelationVar v_eq_value
                                let v_eq_value_lit = match nq with
                                                     | (true, var) -> var
                                                     | (false, _) ->
                                                        let newBool = (!db).mkFreshBooleanVariable ()
                                                        v_eq_value.setBoolvar newBool
                                                        (!db).addTheoryRelation v_eq_value
                                                        newBool

                                // (... /\ value != oldValue)

                                // if we already know that v_eq_value_lit is false, then
                                // there is a conflict (-v_eq_old_value_lit \/ -v_eq_value_lit)
                                if (((!bVal).getValueB v_eq_value_lit) = True) then
                                    let cls = collectLiterals([ Negate v_eq_old_value_lit; Negate v_eq_value_lit; ])
                                    cnflct <- Some (ref (newClauseFromList cls))

                            elif USE_BOUNDS then
//                                 let oldBnds = (!bounds).get v
//
//                                 if BitVector.bvULT intersection.Maximum oldBnds.Lower then
//                                    let cls = collectLiterals([ negPABool;
//                                                                Negate (!bounds).L_explanation.[v];
//                                                                Negate oldExpl;
//                                                                ])
//                                    cnflct <- Some (ref (newClauseFromList cls))
//
//                                 elif cnflct = None && BitVector.bvULT oldBnds.Upper intersection.Minimum then
//                                    let cls = collectLiterals([ negPABool;
//                                                                Negate (!bounds).U_explanation.[v];
//                                                                Negate oldExpl;
//                                                                ])
//                                    cnflct <- Some (ref (newClauseFromList cls))
//                                 else
//                                    //Now we can introduce extractions to block unwanted model assignment attempts.
                                    ()
                    else //value.isConcreteValue

                        if USE_BOUNDS then

//                            let oldBnds = ((!bounds).get v)
//                            let negPABool = rel.getBoolVar
//
//
//                            // This is a special cross-theory case where
//                            // a negatively asserted model assignment
//                            // can refine the bounds slightly.
//
//                            // Note: Previously we had reasons for the lower and upper bound, now we
//                            // refine one of them based on information from a PAPredicate. To make
//                            // this work correctly, we need to introduce a new _bounds_ predicate,
//                            // such that we have oldBnds /\ not PAPredicate => newBoundsPredicate.
//
//                            let (newBnds, newPred, oldExpl) =
//                                if (BitVector.bvEQ oldBnds.Lower value) then
//                                    let newLower = BitVector.bvAdd oldBnds.Lower (BitVector.One oldBnds.Lower.Length)
//                                    (Interval(newLower, oldBnds.Upper),
//                                     (getLowerBoundPredicate db v newLower bVal bvVal bounds),
//                                     (!bounds).L_explanation.[v])
//                                elif (BitVector.bvEQ oldBnds.Upper value) then
//                                    let newUpper = BitVector.bvSub oldBnds.Upper (BitVector.One oldBnds.Upper.Length)
//                                    (Interval(oldBnds.Lower, newUpper),
//                                     (getUpperBoundPredicate db v newUpper bVal bvVal bounds),
//                                     (!bounds).U_explanation.[v])
//                                else
//                                    (oldBnds, TheoryRelation.EmptyThRel, 0)
//
//                            let newBool = newPred.getBoolVar
//                            let newBoolVal = (!bVal).getValueB newBool
//
//                            if newBnds.isEmpty then
//                                let cls = collectLiterals([ negPABool;
//                                                            Negate (!bounds).L_explanation.[v];
//                                                            Negate (!bounds).U_explanation.[v] ])
//                                cnflct <- Some (ref (newClauseFromList cls))
//                            elif newBoolVal = False then
//                                let cls = collectLiterals([ negPABool;
//                                                            Negate (!bounds).L_explanation.[v];
//                                                            Negate (!bounds).U_explanation.[v];
//                                                            newBool ])
//                                cnflct <- Some (ref (newClauseFromList cls))
//                            elif newBoolVal = Undefined && oldBnds <> newBnds then
//                                    // CMW: collectLiterals reverses the order of the literals;
//                                    // we have to make sure that `newBool' is first.
//                                    let cls = collectLiterals [ Negate oldExpl; negPABool; newBool ]
//                                    let ic = newClauseFromList cls
//                                    cnflct <- r.Push bVal bvVal bounds db stats (Imp (ref ic, newBool))
//                            else
//                                 // We can learn that: not (x = a) => x < a \/ x >a
//                                 // which is equivalent to  x=a \/ not x<=a \/ not x>=a
////                                 let x_leq_value = getUpperBoundPredicate db v value bVal pAss bounds
////                                 let value_leq_x = getLowerBoundPredicate db v value bVal pAss bounds
////                                 let gt =  Negate (x_leq_value.getBoolVar)
////                                 let lt = Negate (value_leq_x.getBoolVar)
////                                 let implication = [rel.getBoolVar; gt; lt ]
////                                 let c = newClauseFromList implication
////
////                                 let gtVal = (!bVal).getValueB gt
////                                 let ltVal = (!bVal).getValueB lt
////                                 assert ( (!bVal).getValueB (rel.getBoolVar) = False)
////                                 assert ( gtVal = Undefined || ltVal = Undefined)
////
////                                 if not ((!(!db).Clauses).isStored c) then
////                                     let status = (!db).addAndWatchClause bVal c
////
////                                     match status with
////                                     | Clause.Unsat -> assert(false)
////                                     | Clause.Implication ->
////                                         assert ( (!bVal).getValueB c.[1] = Undefined)
////                                         cnflct <- r.Push bVal pAss bounds db stats (Imp (ref c, c.[1], None))
////                                     | _ -> ()
//                                ()
                                    ()

            if USE_BOUNDS then
                // Bounds theory hook.

                if rel.isBoundsPredicate && (not rel.isPAPredicate || isPositive l) then //AZ: This is to avoid duplicate propagation of x =/= cnst,
                                                                                         //    since it is already handled above.
                    let v = rel.getBoundsPredicateVariable
                    let newBnds = rel.getBoundsPredicateValue (!db).Numerals


                    let args = if isPositive l then (v, l, newBnds)
                               else (v, l, newBnds.Complement())

                    //if isPositive(l) then
                    // Positive BoundsPredicate
                    //let args = (v, rel.getBoolVar, newBnds)
                    let te = r.makeBoundsMA args bounds db stats
                    match te with
                    | (Some(e), None) -> r.pushElement e
                    | (None,Some cRef) -> cnflct <- Some cRef //xTheory conflict
                    | (Some _, Some _) -> UNREACHABLE "Propagation in a conflict state"
                    | _ -> ()

                    let bnds = ((!bounds).get v)
                    if cnflct.IsNone && (fst te).IsSome && bnds.isSingleton then
                        let oldValue = (!bvVal).getValue v
                        let newValue = bnds.Lower

                        if BitVector.bvEQ oldValue newValue then
                            ()
                        else
                            // Note: This is a new RLE theory assignment with bounds theory reasons,
                            // i.e., this is a cross-theory implication. This could create trouble
                            // later, if we assume all reasons are exclusively bounds reasons, or
                            // exclusively MA reasons.

                            let newPred = getModelAssignmentPredicate db v newValue bVal bvVal bounds

                            let newBool = newPred.getBoolVar
                            let (lExpl,uExpl) = (!bounds).getExplanations v

                            // CMW: collectLiterals reverses the order of the literals;
                            // we have to make sure that `newBool' is first.
                            let explanation = newClauseFromList (collectLiterals([ Negate lExpl; Negate uExpl; newBool ]))

                            match (!bVal).getValueB newBool with
                            | True -> assert(false) // AZ: Deriving old knowledge should not be possible here
                            | False ->  cnflct <- Some (ref explanation) //xTheory conflict
                            | Undefined -> //xTheory propagation
                            cnflct <- r.Push bVal bvVal bounds db stats (Imp (ref explanation, newBool))
                        ()
                    ()
//                    else
//                        // Negative BoundsPredicate
//
//                        // CMW: Todo. We should be able to use negative bounds information too,
//                        // but I'm not sure whether we absolutely have to catch this case to
//                        // get enough information for decisions/conflict resolution not to fail.
//                        ()

        cnflct