Home
last modified time | relevance | path

Searched refs:fullterms (Results 1 – 18 of 18) sorted by relevance

/dports/math/eprover/eprover-E-2.0/CLAUSES/
H A Dccl_clauses.h300 void ClausePrintList(FILE* out, Clause_p clause, bool fullterms);
301 void ClausePrintAxiom(FILE* out, Clause_p clause, bool fullterms);
302 void ClausePrintRule(FILE* out, Clause_p clause, bool fullterms);
303 void ClausePrintGoal(FILE* out, Clause_p clause, bool fullterms);
304 void ClausePrintQuery(FILE* out, Clause_p clause, bool fullterms);
306 void ClausePrintLOPFormat(FILE* out, Clause_p clause, bool fullterms);
308 void ClausePrint(FILE* out, Clause_p clause, bool fullterms);
309 void ClausePCLPrint(FILE* out, Clause_p clause, bool fullterms);
310 void ClauseTSTPCorePrint(FILE* out, Clause_p clause, bool fullterms);
311 void ClauseTSTPPrint(FILE* out, Clause_p clause, bool fullterms,
H A Dccl_clauses.c1211 EqnPrint(out, handle, false, fullterms); in ClausePrintAxiom()
1226 EqnPrint(out, handle, true, fullterms); in ClausePrintAxiom()
1256 EqnPrint(out, clause->literals, false, fullterms); in ClausePrintRule()
1261 fullterms); in ClausePrintRule()
1287 EqnListPrint(out, clause->literals, ", ", true, fullterms); in ClausePrintGoal()
1387 ClausePrintQuery(out, clause, fullterms); in ClausePrintLOPFormat()
1391 ClausePrintAxiom(out, clause, fullterms); in ClausePrintLOPFormat()
1408 void ClausePrint(FILE* out, Clause_p clause, bool fullterms) in ClausePrint() argument
1432 ClauseTSTPPrint(out, clause, fullterms, true); in ClausePrint()
1436 ClausePrintLOPFormat(out, clause, fullterms); in ClausePrint()
[all …]
H A Dccl_formula_wrapper.c316 void WFormulaTPTPPrint(FILE* out, WFormula_p form, bool fullterms) in WFormulaTPTPPrint() argument
341 TFormulaTPTPPrint(out, form->terms, form->tformula,fullterms, false); in WFormulaTPTPPrint()
448 void WFormulaTSTPPrint(FILE* out, WFormula_p form, bool fullterms, in WFormulaTSTPPrint() argument
497 ClauseTSTPCorePrint(out, clause, fullterms); in WFormulaTSTPPrint()
503 TFormulaTPTPPrint(out, form->terms, form->tformula,fullterms, false); in WFormulaTSTPPrint()
628 void WFormulaPrint(FILE* out, WFormula_p form, bool fullterms) in WFormulaPrint() argument
633 ClausePrint(out, clause, fullterms); in WFormulaPrint()
643 WFormulaTPTPPrint(out, form, fullterms); in WFormulaPrint()
646 WFormulaTSTPPrint(out, form, fullterms, true); in WFormulaPrint()
H A Dccl_eqn.c818 TBPrintTerm(out, eq->bank, eq->lterm, fullterms); in EqnPrint()
820 TBPrintTerm(out, eq->bank, eq->rterm, fullterms); in EqnPrint()
825 TBPrintTerm(out, eq->bank, eq->lterm, fullterms); in EqnPrint()
836 TBPrintTerm(out, eq->bank, eq->lterm, fullterms); in EqnPrint()
844 TBPrintTerm(out, eq->bank, eq->rterm, fullterms); in EqnPrint()
857 TBPrintTerm(out, eq->bank, eq->lterm, fullterms); in EqnPrint()
859 TBPrintTerm(out, eq->bank, eq->rterm, fullterms); in EqnPrint()
864 TBPrintTerm(out, eq->bank, eq->lterm, fullterms); in EqnPrint()
914 TBPrintTerm(out, eq->bank, eq->lterm, fullterms); in EqnFOFPrint()
920 TBPrintTerm(out, eq->bank, eq->rterm, fullterms); in EqnFOFPrint()
[all …]
H A Dccl_formula_wrapper.h96 void WFormulaTPTPPrint(FILE* out, WFormula_p form, bool fullterms);
99 void WFormulaTSTPPrint(FILE* out, WFormula_p form, bool fullterms,
104 void WFormulaPrint(FILE* out, WFormula_p form, bool fullterms);
H A Dccl_eqnlist.c1222 bool negated, bool fullterms) in EqnListPrint() argument
1228 EqnPrint(out, handle, negated, fullterms); in EqnListPrint()
1234 EqnPrint(out, handle, negated, fullterms); in EqnListPrint()
1251 void EqnListTSTPPrint(FILE* out, Eqn_p list, char* sep, bool fullterms) in EqnListTSTPPrint() argument
1257 EqnTSTPPrint(out, handle, fullterms); in EqnListTSTPPrint()
1263 EqnTSTPPrint(out, handle, fullterms); in EqnListTSTPPrint()
H A Dccl_eqnlist.h96 bool negated, bool fullterms);
97 void EqnListTSTPPrint(FILE* out, Eqn_p list, char* sep, bool fullterms);
H A Dccl_tformulae.c602 void TFormulaTPTPPrint(FILE* out, TB_p bank, TFormula_p form, bool fullterms, bool pcl) in TFormulaTPTPPrint() argument
615 EqnFOFPrint(out, tmp, form->f_code == bank->sig->neqn_code, fullterms, pcl); in TFormulaTPTPPrint()
636 TFormulaTPTPPrint(out, bank, form->args[1], fullterms, pcl); in TFormulaTPTPPrint()
642 TFormulaTPTPPrint(out, bank, form->args[0], fullterms, pcl); in TFormulaTPTPPrint()
651 TFormulaTPTPPrint(out, bank, form->args[0], fullterms, pcl); in TFormulaTPTPPrint()
689 TFormulaTPTPPrint(out, bank, form->args[1], fullterms, pcl); in TFormulaTPTPPrint()
H A Dccl_clausesets.h99 fullterms);
100 void ClauseSetTSTPPrint(FILE* out, ClauseSet_p set, bool fullterms);
H A Dccl_formulasets.c341 void FormulaSetPrint(FILE* out, FormulaSet_p set, bool fullterms) in FormulaSetPrint() argument
349 WFormulaPrint(out, handle, fullterms); in FormulaSetPrint()
H A Dccl_formulasets.h70 bool fullterms);
H A Dccl_eqn.h209 void EqnPrint(FILE* out, Eqn_p eq, bool negated, bool fullterms);
212 void EqnFOFPrint(FILE* out, Eqn_p eq, bool negated, bool fullterms, bool pcl);
213 void EqnTSTPPrint(FILE* out, Eqn_p eq, bool fullterms);
H A Dccl_tformulae.h71 void TFormulaTPTPPrint(FILE* out, TB_p bank, TFormula_p form, bool fullterms, bool pcl);
H A Dccl_clausesets.c793 void ClauseSetPrint(FILE* out, ClauseSet_p set, bool fullterms) in ClauseSetPrint() argument
800 ClausePrint(out, handle, fullterms); in ClauseSetPrint()
818 void ClauseSetTSTPPrint(FILE* out, ClauseSet_p set, bool fullterms) in ClauseSetTSTPPrint() argument
825 ClauseTSTPPrint(out, handle, fullterms, true); in ClauseSetTSTPPrint()
/dports/math/eprover/eprover-E-2.0/LEARN/
H A Dcle_annoterms.h63 fullterms);
H A Dcle_annoterms.c193 void AnnoTermPrint(FILE* out, TB_p bank, AnnoTerm_p term, bool fullterms) in AnnoTermPrint() argument
195 TBPrintTerm(out, bank, term->term, fullterms); in AnnoTermPrint()
/dports/math/eprover/eprover-E-2.0/TERMS/
H A Dcte_termbanks.h154 void TBPrintTerm(FILE* out, TB_p bank, Term_p term, bool fullterms);
H A Dcte_termbanks.c957 void TBPrintTerm(FILE* out, TB_p bank, Term_p term, bool fullterms) in TBPrintTerm() argument
959 if(fullterms) in TBPrintTerm()