Cubicle 1.1.2 documentation and source : Enumsolver_types.add

let add_atom implied (vname, value, mask) =
    try HA.find ha (vname,value)
    with Not_found ->
      let cpt_fois_2 = !cpt_mk_var lsl 1 in
      let ident = mkident vname mask in
      let neg_value = ident.mask land (lnot value) in
      let rec var =
        { vid = !cpt_mk_var ;
          ident = ident;
          pa = pa;
          na = na;
          level = -1;
	  reason = None;
	  seen = false;
	  vpremise = [];
          weight = 0.;}
      and pa = 
	{ aid = cpt_fois_2;
          var = var;
          neg = na;
          value = value;
          is_true = false;
	  watched = Vec.make 10 dummy_clause;
	}
      and na =
	{ aid = cpt_fois_2 + 1;
          var = var;
          neg = pa;
          value = neg_value;
          is_true = false;
	  watched = Vec.make 10 dummy_clause;
        }
      in
      Vec.push ident.ivars var;
      if is_top pa then begin 
        pa.is_true <- true;
        pa.var.level <- 0;
      end;
      if is_bottom pa then begin 
        na.is_true <- true;
        na.var.level <- 0;
      end;
      HA.add ha (vname, value) pa;
      HA.add ha (vname, neg_value) na;
      incr cpt_mk_var;
      new_implied_facts implied var;
      pa