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 :
+ 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
end
else raise (Stop (Timeout (maxvar,bag)));
- let use_age = weight_picks = (iterno / 10 + 1) in
+ let use_age = weight_picks = (iterno / 6 + 1) in
let weight_picks = if use_age then 0 else weight_picks+1
in