1
/**************************************************************/
2
/* ********************************************************** */
4
/* * REDUCTION RULES * */
6
/* * $Module: REDRULES * */
8
/* * Copyright (C) 1996, 1997, 1998, 1999, 2000 * */
9
/* * MPI fuer Informatik * */
11
/* * This program is free software; you can redistribute * */
12
/* * it and/or modify it under the terms of the FreeBSD * */
15
/* * This program is distributed in the hope that it will * */
16
/* * be useful, but WITHOUT ANY WARRANTY; without even * */
17
/* * the implied warranty of MERCHANTABILITY or FITNESS * */
18
/* * FOR A PARTICULAR PURPOSE. See the LICENCE file * */
19
/* * for more details. * */
22
/* $Revision: 1.4 $ * */
24
/* $Date: 2010-02-22 14:09:59 $ * */
25
/* $Author: weidenb $ * */
28
/* * Christoph Weidenbach * */
29
/* * MPI fuer Informatik * */
30
/* * Stuhlsatzenhausweg 85 * */
31
/* * 66123 Saarbruecken * */
32
/* * Email: spass@mpi-inf.mpg.de * */
35
/* ********************************************************** */
36
/**************************************************************/
39
/* $RCSfile: rules-red.h,v $ */
45
#include "subsumption.h"
46
#include "condensing.h"
48
#include "rules-split.h"
49
#include "rules-inf.h"
50
#include "doc-proof.h"
54
/**************************************************************/
56
/**************************************************************/
57
#define CRW_CHECK_STACK stack_SIZE - ((stack_SIZE / 100) * 10)
59
/**************************************************************/
61
/**************************************************************/
63
extern const NAT red_USABLE;
64
extern const NAT red_WORKEDOFF;
65
extern const NAT red_ALL;
68
/**************************************************************/
70
/**************************************************************/
72
static __inline__ BOOL red_WorkedOffMode(NAT Mode)
74
return (Mode == red_WORKEDOFF || Mode == red_ALL);
77
static __inline__ BOOL red_OnlyWorkedOffMode(NAT Mode)
79
return (Mode == red_WORKEDOFF);
82
static __inline__ BOOL red_UsableMode(NAT Mode)
84
return (Mode == red_USABLE || Mode == red_ALL);
87
static __inline__ BOOL red_AllMode(NAT Mode)
89
return (Mode == red_ALL);
97
LIST red_CompleteReductionOnDerivedClauses(PROOFSEARCH, LIST, NAT, int, NAT, int*);
98
CLAUSE red_ReductionOnDerivedClause(PROOFSEARCH, CLAUSE, NAT);
99
CLAUSE red_CompleteReductionOnDerivedClause(PROOFSEARCH, CLAUSE, NAT);
100
LIST red_BackReduction(PROOFSEARCH, CLAUSE, NAT);
101
LIST red_SatUnit(PROOFSEARCH, LIST);
102
LIST red_SatInput(PROOFSEARCH);
103
LIST red_ReduceInput(PROOFSEARCH, LIST);
104
BOOL red_ClauseDeletion(SORTTHEORY, CLAUSE, FLAGSTORE, PRECEDENCE);
105
BOOL red_ExplicitTautology(CLAUSE, FLAGSTORE, PRECEDENCE);
108
void red_CheckSplitSubsumptionCondition(PROOFSEARCH);
111
unsigned long red_GetCRwCalls();
112
unsigned long red_GetCRwSucceeded();