/dports/math/eprover/eprover-E-2.0/TERMS/ |
H A D | cte_signature.h | 140 }SigCell, *Sig_p; typedef 184 Sig_p SigAlloc(SortTable_p sort_table); 185 void SigInsertInternalCodes(Sig_p sig); 186 void SigFree(Sig_p junk); 217 void SigPrint(FILE* out, Sig_p sig); 223 int SigFindMaxUsedArity(Sig_p sig); 224 int SigFindMaxPredicateArity(Sig_p sig); 225 int SigFindMinPredicateArity(Sig_p sig); 226 int SigFindMaxFunctionArity(Sig_p sig); 227 int SigFindMinFunctionArity(Sig_p sig); [all …]
|
H A D | cte_signature.c | 118 Sig_p SigAlloc(SortTable_p sort_table) in SigAlloc() 120 Sig_p handle; in SigAlloc() 200 void SigInsertInternalCodes(Sig_p sig) in SigInsertInternalCodes() 252 void SigFree(Sig_p junk) in SigFree() 651 void SigPrint(FILE* out, Sig_p sig) in SigPrint() 870 int SigFindMaxUsedArity(Sig_p sig) in SigFindMaxUsedArity() 896 int SigFindMaxPredicateArity(Sig_p sig) in SigFindMaxPredicateArity() 927 int SigFindMinPredicateArity(Sig_p sig) in SigFindMinPredicateArity() 958 int SigFindMaxFunctionArity(Sig_p sig) in SigFindMaxFunctionArity() 988 int SigFindMinFunctionArity(Sig_p sig) in SigFindMinFunctionArity() [all …]
|
H A D | cte_typecheck.h | 39 bool TypeCheckConsistent(Sig_p sig, Term_p term); 40 void TypeInferSort(Sig_p sig, Term_p term); 41 void TypeDeclareIsPredicate(Sig_p sig, Term_p term); 42 void TypeDeclareIsNotPredicate(Sig_p sig, Term_p term);
|
H A D | cte_fp_index.h | 69 Sig_p sig; 75 typedef void (*FPLeafPayloadPrint)(FILE* out, PObjTree_p payload, Sig_p sig); 99 Sig_p sig, 103 Sig_p sig, 111 FPIndex_p FPIndexAlloc(FPIndexFunction fp_fun, Sig_p sig, 128 FPLeafPayloadPrint prt_sig, Sig_p sig);
|
H A D | cte_termfunc.h | 52 void TermPrint(FILE* out, Term_p term, Sig_p sig, DerefType deref); 53 void TermPrintArgList(FILE* out, Term_p *args, int arity, Sig_p sig, 56 FunCode TermSigInsert(Sig_p sig, const char* name, int arity, bool 58 Term_p TermParse(Scanner_p in, Sig_p sig, VarBank_p vars); 59 int TermParseArgList(Scanner_p in, Term_p** arg_anchor, Sig_p sig, 115 long VarBankCheckBindings(FILE* out, VarBank_p bank, Sig_p sig); 140 void TermAssertSameSort(Sig_p sig, Term_p t1, Term_p t2);
|
H A D | cte_acterms.h | 57 ACTerm_p ACTermNormalize(Sig_p sig, Term_p term); 58 void ACTermPrint(FILE* out, ACTerm_p term, Sig_p sig); 59 bool TermACEqual(Sig_p sig, Term_p t1, Term_p t2);
|
H A D | cte_typecheck.c | 53 SortType infer_return_sort(Sig_p sig, FunCode f_code) in infer_return_sort() 98 bool TypeCheckConsistent(Sig_p sig, Term_p term) in TypeCheckConsistent() 161 void TypeInferSort(Sig_p sig, Term_p term) in TypeInferSort() 241 void TypeDeclareIsPredicate(Sig_p sig, Term_p term) in TypeDeclareIsPredicate() 262 void TypeDeclareIsNotPredicate(Sig_p sig, Term_p term) in TypeDeclareIsNotPredicate()
|
H A D | cte_subst.h | 60 bool SubstBindingPrint(FILE* out, Term_p var, Sig_p sig, DerefType deref); 61 long SubstPrint(FILE* out, Subst_p subst, Sig_p sig, DerefType deref); 65 void SubstSkolemizeTerm(Term_p term, Subst_p subst, Sig_p sig);
|
H A D | cte_fp_index.c | 190 Sig_p sig, in fp_index_rek_find_unif() 302 Sig_p sig, in fp_index_rek_find_matchable() 513 static char* fp_symbol(Sig_p sig, FunCode symbol) in fp_symbol() 541 PStack_p stack, Sig_p sig) in fp_index_tree_print_node() 574 PStack_p stack, Sig_p sig) in fp_index_tree_print_nodes() 609 PStack_p stack, Sig_p sig) in fp_index_tree_print_edges() 739 Sig_p sig, in dt_index_rek_find_matchable() 822 Sig_p sig, in dt_index_rek_find_unifiable() 1074 Sig_p sig, in FPTreeFindUnifiable() 1099 Sig_p sig, in FPTreeFindMatchable() [all …]
|
H A D | cte_acterms.c | 83 static void ac_collect_args(PTree_p* root, Sig_p sig, FunCode f, in ac_collect_args() 237 ACTerm_p ACTermNormalize(Sig_p sig, Term_p term) in ACTermNormalize() 302 void ACTermPrint(FILE* out, ACTerm_p term, Sig_p sig) in ACTermPrint() 345 bool TermACEqual(Sig_p sig, Term_p t1, Term_p t2) in TermACEqual()
|
H A D | cte_subst.c | 193 bool SubstBindingPrint(FILE* out, Term_p var, Sig_p sig, DerefType in SubstBindingPrint() 225 long SubstPrint(FILE* out, Subst_p subst, Sig_p sig, DerefType deref) in SubstPrint() 349 void SubstSkolemizeTerm(Term_p term, Subst_p subst, Sig_p sig) in SubstSkolemizeTerm()
|
H A D | cte_termfunc.c | 60 static void print_cons_list(FILE* out, Term_p list, Sig_p sig, DerefType deref) in print_cons_list() 95 static Term_p parse_cons_list(Scanner_p in, Sig_p sig, VarBank_p vars) in parse_cons_list() 221 void TermPrint(FILE* out, Term_p term, Sig_p sig, DerefType deref) in TermPrint() 289 void TermPrintArgList(FILE* out, Term_p *args, int arity, Sig_p sig, in TermPrintArgList() 364 FunCode TermSigInsert(Sig_p sig, const char* name, int arity, bool in TermSigInsert() 408 Term_p TermParse(Scanner_p in, Sig_p sig, VarBank_p vars) in TermParse() 517 int TermParseArgList(Scanner_p in, Term_p** arg_anchor, Sig_p sig, in TermParseArgList() 1362 FunCode VarBankCheckBindings(FILE* out, VarBank_p bank, Sig_p sig) in VarBankCheckBindings() 1782 void TermAssertSameSort(Sig_p sig, Term_p t1, Term_p t2) in TermAssertSameSort()
|
/dports/math/eprover/eprover-E-2.0/CLAUSES/ |
H A D | ccl_derivation.h | 158 Sig_p sig; 201 void ClausePushACResDerivation(Clause_p clause, Sig_p sig); 215 Sig_p sig, 219 Sig_p sig, 239 void DerivationStackPCLPrint(FILE* out, Sig_p sig, PStack_p derivation); 242 void DerivedPCLPrint(FILE* out, Sig_p sig, Derived_p derived); 243 void DerivedTSTPPrint(FILE* out, Sig_p sig, Derived_p derived); 244 void DerivedDotPrint(FILE* out, Sig_p sig, Derived_p derived, 252 Derivation_p DerivationAlloc(Sig_p sig); 264 Derivation_p DerivationCompute(PStack_p root_clauses, Sig_p sig); [all …]
|
H A D | ccl_subterm_tree.h | 98 void SubtermTreePrint(FILE* out, SubtermTree_p root, Sig_p sig); 100 void SubtermTreePrintDot(FILE* out, SubtermTree_p root, Sig_p sig); 101 void SubtermTreePrintDummy(FILE* out, SubtermTree_p root, Sig_p sig);
|
H A D | ccl_f_generality.h | 53 Sig_p sig; 68 GenDistrib_p GenDistribAlloc(Sig_p sig); 70 void GenDistribSizeAdjust(GenDistrib_p gd, Sig_p sig);
|
H A D | ccl_global_indices.h | 44 Sig_p sig; 62 Sig_p sig,
|
H A D | ccl_sine.h | 137 Sig_p sig, 160 void DRelPrintDebug(FILE* out, DRel_p rel, Sig_p sig); 161 void DRelationPrintDebug(FILE* out, DRelation_p rel, Sig_p sig);
|
H A D | ccl_subterm_tree.c | 89 void subterm_tree_print_dot(FILE* out, SubtermTree_p root, Sig_p sig) in subterm_tree_print_dot() 432 void SubtermTreePrint(FILE* out, SubtermTree_p root, Sig_p sig) in SubtermTreePrint() 460 void SubtermTreePrintDot(FILE* out, SubtermTree_p root, Sig_p sig) in SubtermTreePrintDot() 505 void SubtermTreePrintDummy(FILE* out, SubtermTree_p root, Sig_p sig) in SubtermTreePrintDummy()
|
H A D | ccl_derivation.c | 535 void ClausePushACResDerivation(Clause_p clause, Sig_p sig) in ClausePushACResDerivation() 752 Sig_p sig, in DerivStackExtractParents() 837 Sig_p sig, in DerivStackExtractOptParents() 1020 void DerivationStackPCLPrint(FILE* out, Sig_p sig, PStack_p derivation) in DerivationStackPCLPrint() 1130 void DerivationStackTSTPPrint(FILE* out, Sig_p sig, PStack_p derivation) in DerivationStackTSTPPrint() 1252 void DerivedPCLPrint(FILE* out, Sig_p sig, Derived_p derived) in DerivedPCLPrint() 1317 void DerivedTSTPPrint(FILE* out, Sig_p sig, Derived_p derived) in DerivedTSTPPrint() 1494 void DerivedDotPrint(FILE* out, Sig_p sig, Derived_p derived, in DerivedDotPrint() 1694 Derivation_p DerivationAlloc(Sig_p sig) in DerivationAlloc() 2099 Derivation_p DerivationCompute(PStack_p root_clauses, Sig_p sig) in DerivationCompute() [all …]
|
/dports/math/eprover/eprover-E-2.0/LEARN/ |
H A D | cle_patterns.h | 57 Sig_p sig; /* For alpha-ranks and potentially other 76 PatternSubst_p PatternSubstAlloc(Sig_p sig); 77 PatternSubst_p PatternDefaultSubstAlloc(Sig_p sig); 114 Term_p term, Sig_p sig); 123 Sig_p old_sig, Sig_p new_sig,
|
H A D | cle_tsmio.h | 45 evalweights[], ExampleSet_p examples, Sig_p sig, 51 char* kb, Sig_p sig, ClauseSet_p target, long 55 kb, Sig_p sig, ClauseSet_p target, long sel_no,
|
H A D | cle_kbinsert.h | 45 long KBAxiomsInsert(ExampleSet_p set, ClauseSet_p axioms, Sig_p sig, 50 AnnoSet_p examples, Sig_p res_sig);
|
H A D | cle_flatannoterms.h | 79 void FlatAnnoTermPrint(FILE* out, FlatAnnoTerm_p term, Sig_p sig); 85 void FlatAnnoSetPrint(FILE* out, FlatAnnoSet_p set, Sig_p sig);
|
H A D | cle_tsmio.c | 243 evalweights[], ExampleSet_p examples, Sig_p sig, in ExampleSetPrepare() 282 char* kb, Sig_p sig, ClauseSet_p target, long in ExampleSetFromKB() 330 kb, Sig_p sig, ClauseSet_p target, long sel_no, in TSMFromKB()
|
/dports/math/eprover/eprover-E-2.0/HEURISTICS/ |
H A D | che_axiomscan.h | 47 bool ClauseScanAC(Sig_p sig, Clause_p clause); 48 bool ClauseSetScanAC(Sig_p sig, ClauseSet_p set);
|