Home
last modified time | relevance | path

Searched refs:CPInitial (Results 1 – 9 of 9) sorted by relevance

/dports/math/eprover/eprover-E-2.0/CLAUSES/
H A Dccl_clausefunc.c218 ClauseDelProp(clause, CPInitial|CPLimitedRW); in ClauseRemoveSuperfluousLiterals()
329 ClauseDelProp(clause, CPInitial|CPLimitedRW); in ClauseRemoveACResolved()
H A Dccl_context_sr.c85 ClauseDelProp(clause, CPInitial|CPLimitedRW); in ClauseContextualSimplifyReflect()
H A Dccl_formula_wrapper.c298 FormulaSetProp(handle, CPInitial|CPInputFormula); in WFormulaTPTPParse()
426 FormulaSetProp(handle, initial|CPInitial); in WFormulaTSTPParse()
H A Dccl_clauses.h45 CPInitial = 1, /* Initial clause */ enumerator
46 CPInputFormula = 2*CPInitial, /* _Really_ initial
H A Dccl_subsumption.c1174 ClauseDelProp(clause, CPInitial|CPLimitedRW); in ClausePositiveSimplifyReflect()
1225 ClauseDelProp(clause, CPInitial|CPLimitedRW); in ClauseNegativeSimplifyReflect()
H A Dccl_rewrite.c1109 ClauseDelProp(clause, CPInitial); in ClauseComputeLINormalform()
H A Dccl_clauses.c1842 ClauseSetProp(handle, CPInitial|input); in ClauseParse()
/dports/math/eprover/eprover-E-2.0/HEURISTICS/
H A Dche_prio_funs.c731 if(ClauseIsAnyPropSet(clause, CPInitial|CPIsSOS)) in PrioFunSimulateSOS()
753 if(ClauseIsAnyPropSet(clause, CPInitial|CPIsSOS)) in PrioFunDeferSOS()
/dports/math/eprover/eprover-E-2.0/CONTROL/
H A Dcco_proofproc.c1238 ClauseSetProp(new, CPInitial); in ProofStateInit()