(*
This file is part of the first order theorem prover Darwin
Copyright (C) 2005, 2006
              The University of Iowa

This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License
as published by the Free Software Foundation; either version 2
of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
*)


exception FOF of bool

exception CLAUSIFIER_RESOURCE_OUT

exception NO_SOLUTION of string

exception PARSE_ERROR




(*** Debug ***)



let debug = false

let stable_derivation = false




(*** Version ***)



let version = "Darwin 1.3"





(*** Preprocessing Resolution ***)



let resolvent_max_size = 3
let resolvents_max_number = 1000





(*** Partial Context Unifiers ***)



let max_cached_partial_context_unifiers = 50000




(*** Candidates ***)



let max_unprocessed_assert_candidates = 0
let max_assert_candidates = 100000
let max_assert_lookahead = 50000
let max_assert_lookahead_exceeding = 10000

let max_unprocessed_split_candidates = 100000




(*** Clause Utility ***)



let decay_clause_utility_interval = 100
let decay_clause_utility_ratio = 2




(*** Lemmas ***)



let lemma_max_constraints = 10000





(*** Restart with Jumping ***)



let jumping_min_distance = 5

let jumping_check_every_splits = 50

let jumping_time_delta = 0.1




(*** Finite Model Generation ***)



let fd_static_symmetry_reduction = true

let fd_use_canonicity = fd_static_symmetry_reduction && true

let fd_use_term_definitions = true

let fd_use_definitions = false

let fd_use_diff = true

let fd_instantiate_totality_axiom = true