Commit 70914ae2 authored by Pietro Abate's avatar Pietro Abate
Browse files

Handling few basic cases directly in Tallying.norm

micro performance improvement
parent d3b48589
......@@ -3008,7 +3008,6 @@ module Tallying = struct
if DescrSet.mem t mem || is_empty t then begin
(*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat end else begin
(*
if is_empty t then CS.sat
(* if there is only one variable then is it A <= 0 or 1 <= A *)
else if is_var t then
......@@ -3017,7 +3016,7 @@ module Tallying = struct
CS.singleton s
(* if there are no vars, and it is not empty then unsat *)
else if no_var t then CS.unsat
else *) begin
else begin
let mem = DescrSet.add t mem in
let aux single norm_aux acc l = big_prod (toplevel single norm_aux mem) acc l in
......
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