let monster = 100;;
-module Paramod (B : Terms.Blob) = struct
+module type Paramod =
+ sig
+ type t
+ type input
+ type szsontology =
+ | Unsatisfiable of (t Terms.bag * int * int list) list
+ | GaveUp
+ | Error of string
+ | Timeout of int * t Terms.bag
+ type bag = t Terms.bag * int
+ val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
+ val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
+ val paramod :
+ useage:bool ->
+ max_steps:int ->
+ ?timeout:float ->
+ bag ->
+ g_passives:t Terms.unit_clause list ->
+ passives:t Terms.unit_clause list -> szsontology
+ end
+
+module Paramod (B : Orderings.Blob) = struct
+ type t = B.t
+ type input = B.input
type szsontology =
| Unsatisfiable of (B.t Terms.bag * int * int list) list
| GaveUp
module IDX = Index.Index(B)
module Sup = Superposition.Superposition(B)
module Utils = FoUtils.Utils(B)
- module Order = Orderings.Orderings(B)
+ module Order = B
module WeightOrderedPassives =
struct
type t = B.t Terms.passive_clause
* new'= demod A'' new *
* P' = P + new' *)
debug "Forward infer step...";
+ debug ("Number of actives : " ^ (string_of_int (List.length (fst actives))));
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
debug
(Printf.sprintf "Number of passives : %d"
(passive_set_cardinal passives));
- given_clause ~noinfer
+ given_clause ~useage ~noinfer
bag maxvar iterno weight_picks max_steps timeout
actives passives g_actives g_passives
;;
- let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
let initial_timestamp = Unix.gettimeofday () in
let passives =
add_passive_clauses ~no_weight:true passive_empty_set passives
let g_actives = [] in
let actives = [], IDX.DT.empty in
try
- given_clause ~noinfer:false
+ given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
with
| Sup.Success (bag, _, (i,_,_,_)) ->