microsoft
/
mcBV
зеркало из https://github.com/microsoft/mcBV.git
1
0
Форкнуть 0
Код Задачи Пакеты Проекты Релизы Вики Активность

formatting/style/whitespace

This commit is contained in:
Christoph M. Wintersteiger 2016-09-13 16:06:43 +01:00
Родитель 3a6520f7da
Коммит 382a6fcb98
4 изменённых файлов: 77 добавлений и 95 удалений
Показать статистику Скачать Patch файл Скачать Diff файл Показать все файлы Свернуть все файлы

2
DataBase.fs
Просмотреть файл

@ -114,7 +114,7 @@ type Database = class
assert(not (tDB.isIntroduced t))
let index = tDB.add t
(!this.Statistics).NewThLiteral()
for v in t.variableArguments do
(!this.Watches).watchBV v index
verbose <| (lazy (sprintf "X New theory relation: %s" (t.ToString(this.Numerals))))

8
RLEBVTheory.fs
Просмотреть файл

@ -353,25 +353,25 @@ let tEvaluate1U (s:State) (tRel:Ref<TheoryRelation>) =
let holds = tHolds (!tRel) s.bvVal s.numeralDB
if holds <> Undefined then
let (expl, l) = tGetImplication s tRel holds
s.Push (Imp (ref expl, l))
s.Push (Imp (ref expl, l))
| Z3_decl_kind.Z3_OP_ULEQ ->
let bVal = (!pVal).getValueB boolVar
let holds = tHolds (!tRel) s.bvVal s.numeralDB
match bVal with
| True ->
| True ->
if holds = False then
let c = Negate (!tRel).getBoolVar :: (tGetAntecedents s tRel)
s.SetConflict (Some (ref (newClauseFromList c)))
elif holds = True then
(!s.bVal).setValueT boolVar (!s.trail).getNumDecisions |> ignore
| False ->
| False ->
if holds = True then
let c = (!tRel).getBoolVar :: (tGetAntecedents s tRel)
s.SetConflict (Some (ref (newClauseFromList c)))
elif holds = False then
(!s.bVal).setValueT (Negate boolVar) (!s.trail).getNumDecisions |> ignore
| _ ->
| _ ->
if holds <> Undefined then
let (expl, l) = tGetImplication s tRel holds
s.Push (Imp (ref expl, l))

16
Trail.fs
Просмотреть файл

@ -1,6 +1,6 @@
module Trail
open Microsoft.Z3
open Util
open Stats
open Interval
@ -494,11 +494,11 @@ type Trail (sz:int) =
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.
@ -569,16 +569,6 @@ type Trail (sz:int) =
// ()
()
if USE_BOUNDS then
// Bounds theory hook.

146
WatchManager.fs
Просмотреть файл

@ -18,8 +18,8 @@ type OccurenceList = int []
//| OFFSET | p_0 | ... |p_{count-1}| trash |
//Returns a pair of (newWatch, clauseStatus)/numNonFalseWatches)/
let findWatch (pl:Literal) (c:Clause) (v:Ref<BooleanValuation>) =
let size = getSize(c)
let findWatch (pl:Literal) (c:Clause) (v:Ref<BooleanValuation>) =
let size = getSize(c)
let npl = -pl;
assert (size >= 2)
@ -35,10 +35,10 @@ let findWatch (pl:Literal) (c:Clause) (v:Ref<BooleanValuation>) =
| True -> (c.[1], Sat) // Satisfied clause.
// This is wrong:
// | False -> (c.[1], 0) // Conflict, c.[1] is the "conflicting literal"
| _ ->
| _ ->
let mutable i = 3
let mutable found = false
// [ U, F ] or [ F F ]
while (not found && i <= size) do
@ -59,7 +59,7 @@ let findWatch (pl:Literal) (c:Clause) (v:Ref<BooleanValuation>) =
(c.[1], Implication) // Implication; invariant: implied literals is at c.[1]
let findTwoWatches (c:Clause) (v:Ref<BooleanValuation>) =
let findTwoWatches (c:Clause) (v:Ref<BooleanValuation>) =
let size = getSize(c)
assert (size >= 2)
let mutable i = 0
@ -76,7 +76,7 @@ let findTwoWatches (c:Clause) (v:Ref<BooleanValuation>) =
i <- size + 1
else
i <- i + 1
if v(c.[2]) = False then
i <- 3
while i <= size do
@ -104,14 +104,14 @@ let snapCount = 2
let wolOffset = 3
type WatchManager private (numOfVariables:int, initWLSize:int) =
type WatchManager private (numOfVariables:int, initWLSize:int) =
let reallocCoefficient = 2.0
new (numOfVariables:int, initWLSize:int, tDB:Ref<TheoryDB>) as this =
WatchManager(numOfVariables, initWLSize)
then
this.initializeWatchLists tDB ()
member val private allocated = 2*numOfVariables with get, set
member val private inUse = numOfVariables with get, set
@ -120,35 +120,35 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
member val private inTempMode = false with get, set
member val private snapshot = -1 with get, set
member r.emptyWatchList = [|0; 0|]
member r.emptyWatchList = [|0; 0|]
member r.initializeWatchLists (fThDB:Ref<TheoryDB>) () =
r.lists <- [| for i in 0 .. r.allocated - 1 do yield Array.create initWLSize -1 |]
for i in 0 .. r.allocated - 1 do
r.setSz i (initWLSize - r.offset) |> ignore
r.setCnt i 0 |> ignore
for i in 0 .. (!fThDB).count - 1 do
for i in 0 .. (!fThDB).count - 1 do
let t = ((!fThDB).getThRelationByIndex i)
for varg in t.variableArguments do
r.watchBV varg i
member r.getIndex(l:Literal) :int =
let ind = if l > 0 then
let ind = if l > 0 then
2*l - 1
elif l < 0 then
elif l < 0 then
2 * (-l - 1)
else
else
-1
assert (r.validIndex ind)
ind
member r.reallocate() =
member r.reallocate() =
let newSize = int (reallocCoefficient * float r.allocated)
r.reallocate (newSize, initWLSize)
member r.reallocate (newSize:int, wlSize:int)=
assert(newSize > r.allocated)
r.lists <- Array.append r.lists [|for i in 0 .. newSize - r.allocated - 1 do yield Array.create wlSize -1 |]
@ -158,37 +158,37 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
r.setSz i (wlSize - r.offset) |> ignore
r.setCnt i 0 |> ignore
member r.newVarToWatch (var:Var) =
member r.newVarToWatch (var:Var) =
assert (not r.inTempMode ||var = r.inUse + 1)
if r.inUse * 2 >= r.allocated then
r.reallocate()
r.inUse <- r.inUse + 1
member r.validIndex ind = ind > -1 && ind < 2*r.inUse && r.inUse < r.allocated
//To be stand alone functions over WatchList/OccurenceList
member private r.getSz(ind:int) :int =
r.lists.[ind].[sizeInd]
member r.getSize(l:int) :int =
member r.getSize(l:int) :int =
let ind = r.getIndex(l)
r.getSz(ind)
member r.setSz(ind:int) (s:int) :int =
member r.setSz(ind:int) (s:int) :int =
assert ( ind > -1 && ind < r.allocated)
r.lists.[ind].[sizeInd] <- s
r.lists.[ind].[sizeInd]
member private r.getCnt(ind:int)=
assert (r.validIndex ind)
r.lists.[ind].[countInd]
member r.getCount(l:Literal) : int =
let ind = r.getIndex(l)
r.getCnt(ind)
member private r.setCnt (ind:int) (c:int) : int =
assert ( ind > -1 && ind < r.allocated)
r.lists.[ind].[countInd] <- c
@ -197,7 +197,7 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
member r.setCount (l:Literal) (c:int) =
let ind = r.getIndex(l)
r.setCnt ind c
member private r.incrCnt (ind:int) : int =
assert (r.validIndex ind)
r.lists.[ind].[countInd] <- r.lists.[ind].[countInd] + 1
@ -208,84 +208,81 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
let idx = r.getIndex bvVar
let mutable found = false
let cnt = r.getCnt idx
let cnt = r.getCnt idx
for i in 0 .. cnt - 1 do
if not found && r.getPtr idx i = ptr then
found <- true
if i < cnt - 1 then
r.setPtr idx i (r.getPtr idx (cnt - 1))
r.setPtr idx (cnt - 1) -1
r.setCnt idx (cnt - 1) |> ignore
assert(found)
member r.getPtr (ind:int) (i:int) :int =
member r.getPtr (ind:int) (i:int) :int =
assert ( r.validIndex ind && 0 <= i && i < r.getCnt ind)
r.lists.[ind].[r.offset + i]
member r.setPtr (ind:int) (i:int) (ptr:int) : Unit =
member r.setPtr (ind:int) (i:int) (ptr:int) : Unit =
assert ( r.validIndex ind && 0 <= i && i <= r.getCnt ind)
r.lists.[ind].[r.offset + i] <- ptr
member r.getPointer (l:Literal) (i:int) :int =
let ind = r.getIndex l
member r.getPointer (l:Literal) (i:int) :int =
let ind = r.getIndex l
r.getPtr ind i
member r.setPointer (l:Literal) (ptr:int) =
member r.setPointer (l:Literal) (ptr:int) =
let ind = r.getIndex(l)
assert (ind > -1 && ind < r.allocated)//if ind > -1 then
let cnt = r.getCnt ind
if cnt >= r.getSz ind then
r.reallocateList ind |> ignore
r.setPtr ind cnt ptr
r.setPtr ind cnt ptr
r.incrCnt(ind) |> ignore
//Initializing/Migrating the watches
member r.watchBool (l:Literal) (c:int) : Unit =
member r.watchBool (l:Literal) (c:int) : Unit =
assert (l<>0)
r.setPointer -l c
//Initializing the occurences
member r.watchBV (v:Var) (t:int) : Unit =
member r.watchBV (v:Var) (t:int) : Unit =
assert (v <> 0)
r.setPointer v t
member r.watchBVInTmpMode (v:Var) (t:int) : Unit =
member r.watchBVInTmpMode (v:Var) (t:int) : Unit =
assert (v <> 0)
assert (r.inTempMode)
let idx = r.getIndex v
let mutable found = false
let cnt = r.getCnt idx
let cnt = r.getCnt idx
for i in 0 .. cnt - 1 do
if not found && r.getPtr idx i = t then
found <- true
if not found then
r.setPointer v t
member r.getWatchList (l:Literal) :WatchList =
member r.getWatchList (l:Literal) :WatchList =
assert (l <> 0)
let ind = r.getIndex(l)
assert (ind > -1)//if ind > -1 then
r.lists.[ind]
member r.reallocateList (ind:int) :int =
assert (r.validIndex ind)
let size = r.getSz(ind)
assert(size > 0)
let nSize = 2*size
let nSize = 2*size
r.lists.[ind] <- Array.append r.lists.[ind] (Array.create size -1)
r.setSz ind nSize
member r.printThWatch (nDB:Ref<NumeralDB>) (thDB:Ref<TheoryDB>) (l:Literal) =
let ind = r.getIndex(l)
let cnt = r.getCnt(ind)
let cnt = r.getCnt(ind)
if cnt = 0 then
printfn "%d:bv: None." l
else
@ -294,16 +291,16 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
let cPtr = r.getPtr ind k
let tRel = !((!thDB).getThRelRef cPtr)
printfn " %d : %s " cPtr (tRel.ToString nDB) //(clauseToString (!(cDB.getClauseRef cPtr)))
member r.printBoolWatch (cDB:Ref<ClauseDB>) (l:Literal) =
let ind = r.getIndex(l)
let cnt = r.getCnt(ind)
// printfn "Currently watching clauses for literal %d: " l
if cnt = 0 then
printfn "%d: None." l
else
printfn "%d: " l
printfn "%d: " l
for k in 0 .. cnt - 1 do
let cPtr = r.getPtr ind k
printfn " %d : %s " cPtr (clauseToString (!((!cDB).getClauseRef cPtr)))
@ -314,22 +311,22 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
r.printBoolWatch cDB l
else
r.printThWatch nDB tDB l
member r.setSnapCnt (ind:int) =
member r.setSnapCnt (ind:int) =
assert (r.inTempMode)
assert ( ind > -1 && ind < r.allocated)
r.lists.[ind].[snapCount] <- r.getCnt ind
member r.resetSnapCnt (ind:int) =
member r.resetSnapCnt (ind:int) =
assert (r.inTempMode)
assert ( r.validIndex ind)
r.lists.[ind].[snapCount] <- - 1
member r.getSnapCnt (ind:int) =
member r.getSnapCnt (ind:int) =
assert ( ind > -1 && ind < r.allocated)
r.lists.[ind].[snapCount]
member r.resetListToSnapCnt (ind:int) =
member r.resetListToSnapCnt (ind:int) =
assert (r.inTempMode)
assert ( ind > -1 && ind < r.allocated)
let snap = r.getSnapCnt ind
@ -342,17 +339,17 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
member r.getInUse = r.inUse
member r.enterTempModeOld () =
member r.enterTempModeOld () =
assert(not r.inTempMode)
assert(r.snapshot = -1)
r.inTempMode <- true
r.inTempMode <- true
for i in 1 .. r.inUse do
r.setSnapCnt (r.getIndex i)
r.setSnapCnt (r.getIndex -i)
r.snapshot <- r.inUse
member r.enterTempMode (newMaxVar:Var) =
member r.enterTempMode (newMaxVar:Var) =
assert(not r.inTempMode)
assert(r.snapshot = -1)
r.inTempMode <- true
@ -365,7 +362,7 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
for i in 0 .. r.allocated - 1 do
r.setSz i (initSz - r.offset) |> ignore
r.setCnt i 0 |> ignore
member r.leaveTempMode (highestVarInUse:Var) =
assert(r.inTempMode)
//assert(r.snapshot >= 0)
@ -385,30 +382,30 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
r.setSz indB (initWLSize - r.offset) |> ignore
r.setCnt indB 0 |> ignore
for i in 1 .. r.snapshot - 1 do
r.resetListToSnapCnt (r.getIndex i)
r.resetListToSnapCnt (r.getIndex -i)
r.inUse <- r.snapshot
r.snapshot <- -1
r.inTempMode <- false
member r.fastForward (orig:Ref<WatchManager>) =
member r.fastForward (orig:Ref<WatchManager>) =
let oInUse = (!orig).getInUse
if r.inUse < oInUse then r.inUse <- oInUse
if r.inUse >= r.allocated then r.reallocate (r.inUse, 3)
assert (r.inUse = oInUse)
// member r.watchNewClause (pCls:Ref<Clause>) (pVal:Ref<Valuation>) (pT:Ref<Trail>) =
assert (r.inUse = oInUse)
// member r.watchNewClause (pCls:Ref<Clause>) (pVal:Ref<Valuation>) (pT:Ref<Trail>) =
// let mutable inConflict = false
// let mutable newState = null
// if getSize(!pCls) = 1 then
// match (!pVal).getVal((!pCls).[1]) with
// | False -> inConflict <- true
// newState <- Conflict (pT, pCDB, pCls)
// | Undefined -> trail.push (cDB.getClauseRef i) (!pCls).[1] |> ignore
// | Undefined -> trail.push (cDB.getClauseRef i) (!pCls).[1] |> ignore
// | True -> () //Already True, and therefore on the trail
// else
// match findWatch -(!pCls).[1] !pCls pVal with
@ -416,21 +413,16 @@ type WatchManager private (numOfVariables:int, initWLSize:int) =
// w.watchBool (!pCls).[2] i |>ignore
// | _ -> match findWatch -(!pCls).[1] !pCls pVal with
// | (_, Clause.Unsat) -> w.watchBool (!pCls).[1] i |>ignore
// w.watchBool (!pCls).[2] i |>ignore
// w.watchBool (!pCls).[2] i |>ignore
// inConflict <- true
// newState <- Conflict (pT, pCDB, pCls)
// | (_, Implication) ->
// | (_, Implication) ->
// w.watchBool (!pCls).[1] i |>ignore
// w.watchBool (!pCls).[2] i |>ignore
// if (!pVal).getVal((!pCls).[1]) = Undefined then //this should be the invariant
// trail.push (cDB.getClauseRef i) (!pCls).[1]|> ignore
// trail.push (cDB.getClauseRef i) (!pCls).[1]|> ignore
// | _ -> w.watchBool (!pCls).[1] i |>ignore
// w.watchBool (!pCls).[2] i |>ignore
//Watch literal l in clause c