Cubicle 1.1.2 documentation and source : Solver_types.make

let make_var =
  fun lit ->
    let lit, negated = normal_form lit in
    try MA.find lit !ma, negated 
    with Not_found ->
      let cpt_fois_2 = !cpt_mk_var lsl 1 in
      let rec var  = 
	{ vid = !cpt_mk_var; 
	  pa = pa;
	  na = na; 
	  level = -1;
	  reason = None;
	  weight = 0.;
	  seen = false;
	  vpremise = [];
	}
      and pa = 
	{ var = var; 
	  lit = lit;
	  watched = Vec.make 10 dummy_clause; 
	  neg = na;
	  is_true = false;
	  aid = cpt_fois_2 (* aid = vid*2 *) }
      and na = 
	{ var = var;
	  lit = Literal.LT.neg lit;
	  watched = Vec.make 10 dummy_clause;
	  neg = pa;
	  is_true = false;
	  aid = cpt_fois_2 + 1 (* aid = vid*2+1 *) } in 
      ma := MA.add lit var !ma;
      incr cpt_mk_var;
      var, negated