Commit f2b424c6 authored by Ranadeep Biswas's avatar Ranadeep Biswas
Browse files

Fix root transaction info

parent a0c50601
......@@ -39,16 +39,19 @@ impl CNF {
let mut literal_map = HashMap::new();
for mut clause in self.clauses.drain(..).rev().skip(1) {
let solver_clause : Vec<_> = clause.drain(..).map(|(sign, literal)| {
let solver_lit = literal_map
.entry(literal)
.or_insert_with(|| solver.new_lit());
if sign {
*solver_lit
} else {
!*solver_lit
}
}).collect();
let solver_clause: Vec<_> = clause
.drain(..)
.map(|(sign, literal)| {
let solver_lit = literal_map
.entry(literal)
.or_insert_with(|| solver.new_lit());
if sign {
*solver_lit
} else {
!*solver_lit
}
})
.collect();
solver.add_clause(solver_clause);
}
......
......@@ -272,6 +272,8 @@ impl Verifier {
if event.success {
if event.write {
write_info.insert(event.variable);
// all variable is initialized at root transaction
root_write_info.insert(event.variable);
} else {
let &(wr_i_node, wr_i_transaction, _) =
write_map.get(&(event.variable, event.value)).unwrap();
......
Markdown is supported
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