type counter = Counter.counter
type config = Config.config
type statistic = Statistic.statistic
type bound = Bound.bound
type var = Var.var
type literal = Term.literal
type clause = Term.clause
type subst = Subst.subst
type state = State.state
type context_unifier_space = Context_unifier.context_unifier_space
type context_partners = Context_unifier.context_partners
type context_partner = Context.element
type input_partner = Context_unifier.input_partner
type raw_context_unifier = Context_unifier.raw_context_unifier
type problem_literals = Problem_literals.problem_literals
type candidate_type = Context_unifier.candidate_type
type space_registry = {
config: config;
bound: bound;
counter: counter;
}
exception UNSATISFIABLE = Context_unifier.UNSATISFIABLE
let get_id space_registry =
try
Counter.next space_registry.counter
with
| Counter.OVERFLOW ->
raise (Const.NO_SOLUTION "Context_unifier_space.create_space: context unifier space id overflow")
let create (config: config) (bound: bound) : space_registry =
{
config = config;
bound = bound;
counter = Counter.create ()
}
let create_input_partners (problem_literals: problem_literals) (clause: clause) : input_partner array =
Array.mapi
(fun index literal ->
Problem_literals.register_literal problem_literals literal index
)
(Array.of_list clause)
let create_ordering (input_partners: input_partner array) : int array =
let ordering =
Array.mapi
(fun i _ -> i)
input_partners
in
Array.sort
(fun x y ->
compare
(Stack.size input_partners.(x).Context_unifier.ip_context_partners)
(Stack.size input_partners.(y).Context_unifier.ip_context_partners)
)
ordering;
ordering
let create_space' ~(register: bool) (space_registry: space_registry)
(problem_literals: problem_literals)
(process_close_candidate: raw_context_unifier -> unit)
(process_assert_candidate: raw_context_unifier -> bool)
(process_split_candidate: raw_context_unifier -> unit)
(is_element_incomplete_assert: Context.element -> bool)
(is_element_incomplete_split: Context.element -> bool)
(clause: clause)
(is_lemma: bool)
: context_unifier_space =
let input_partners =
create_input_partners problem_literals clause
in
let ordering =
create_ordering input_partners
in
let input_vars =
Array.map
(fun partner -> partner.Context_unifier.ip_vars)
input_partners
in
let vars =
Array.fold_left
(fun acc vars ->
Tools.lists_merge Subst.var_equal acc vars
)
[]
input_vars
in
let shared_subst_vars =
Tools.lists_shared
Subst.var_equal
(Array.to_list input_vars)
in
let local_subst_vars =
Array.fold_left
(fun acc vars ->
List.fold_left
(fun acc var ->
if List.exists (fun var' -> Subst.var_equal var var') shared_subst_vars then
acc
else
var :: acc;
)
acc
vars
)
[]
input_vars
in
let id =
get_id space_registry
in
let context_unifier_space =
Context_unifier.create_space
id clause vars shared_subst_vars local_subst_vars input_partners ordering
process_close_candidate process_assert_candidate process_split_candidate
is_element_incomplete_assert is_element_incomplete_split is_lemma
in
if register then begin
Array.iter
(fun input_partner ->
Problem_literals.register_input_partner
problem_literals input_partner context_unifier_space
)
input_partners;
end;
if
is_lemma
||
List.length clause = 1
then
()
else begin
try
let context_partners =
Array.map
(fun input_partner ->
if Const.debug then begin
if Stack.size input_partner.Context_unifier.ip_context_partners > 1 then
failwith "Context_unifier_space.create_space"
end;
Stack.top input_partner.Context_unifier.ip_context_partners
)
input_partners
in
let candidate =
Context_unifier.create_context_unifier
context_unifier_space context_partners false
in
let subst =
Context_unifier.recompute_unifier ~recompute:false candidate
in
begin
match Context_unifier_check.check_split space_registry.config space_registry.bound
subst context_unifier_space context_partners false with
| None ->
()
| Some candidate ->
context_unifier_space.Context_unifier.cus_process_split_candidate candidate;
end;
with
| Not_found ->
()
end;
context_unifier_space
let create_space ?(register: bool = true) (space_registry: space_registry)
(problem_literals: problem_literals)
(clause: clause)
(process_close_candidate: raw_context_unifier -> unit)
(process_assert_candidate: raw_context_unifier -> bool)
(process_split_candidate: raw_context_unifier -> unit)
(is_element_incomplete_assert: Context.element -> bool)
(is_element_incomplete_split: Context.element -> bool)
(is_lemma: bool)
: context_unifier_space =
match clause with
| [] ->
failwith "Context_unifier_space.create"
| _ ->
create_space' ~register:register space_registry problem_literals
process_close_candidate process_assert_candidate process_split_candidate
is_element_incomplete_assert is_element_incomplete_split
clause is_lemma
let backtrack (context_unifier_space: context_unifier_space) : unit =
let input_partners =
context_unifier_space.Context_unifier.cus_input_partners
in
let ordering =
context_unifier_space.Context_unifier.cus_input_partners_ordering
in
for i = 1 to Array.length input_partners - 1 do
let input_partner_to_move =
input_partners.(ordering.(i))
in
match input_partner_to_move.Context_unifier.ip_resolved with
| Some _ ->
()
| None ->
let rec insert_at j =
if j = i then
()
else if
match input_partners.(ordering.(j)).Context_unifier.ip_resolved with
| Some _ -> true
| None -> false
then
insert_at (j + 1)
else if
(Stack.size input_partner_to_move.Context_unifier.ip_context_partners)
>=
(Stack.size input_partners.(ordering.(j)).Context_unifier.ip_context_partners)
then
insert_at (j + 1)
else begin
let swap = ordering.(i)
in
for k = i downto j + 1 do
ordering.(k) <- ordering.(k - 1);
done;
ordering.(j) <- swap;
end
in
insert_at 0
done;
if Const.debug then begin
for i = 1 to Array.length input_partners - 1 do
if
(
(Stack.size input_partners.(ordering.(i)).Context_unifier.ip_context_partners)
>=
(Stack.size input_partners.(ordering.(i - 1)).Context_unifier.ip_context_partners)
)
||
(match input_partners.(ordering.(i)).Context_unifier.ip_resolved with
| Some _ -> true
| None -> false
)
||
(match input_partners.(ordering.(i - 1)).Context_unifier.ip_resolved with
| Some _ -> true
| None -> false
)
then
()
else begin
for i = 0 to Array.length input_partners - 1 do
print_int
(Stack.size input_partners.(ordering.(i)).Context_unifier.ip_context_partners);
print_newline ();
done;
failwith "Context_unifier_space.backtrack: order not preserved"
end
done
end