~ubuntu-branches/ubuntu/oneiric/spass/oneiric : revision 4

1

/**************************************************************/

2

/* ********************************************************** */

3

/* * * */

4

/* * EXTENDED MODAL LOGICS ROUTINES * */

5

/* * * */

6

/* * $Module: EML * */

7

/* * * */

8

/* * * */

9

/* $Revision: 1.7 $ * */

10

/* $State: Exp $ * */

11

/* * This program is free software; you can redistribute * */

12

/* * it and/or modify it under the terms of the FreeBSD * */

13

/* * Licence. * */

14

/* * * */

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. * */

20

/* $Date: 2010-02-22 14:09:58 $ * */

21

/* $Author: weidenb $ * */

22

/* * * */

23

/* * Contact: * */

24

/* * Renate Schmidt * */

25

/* * School of Computer Science * */

26

/* * University of Manchester * */

27

/* * Oxford Rd, Manchester M13 9PL, UK * */

28

/* * Email: Renate.Schmidt@manchester.ac.uk * */

29

/* * * */

30

/* ********************************************************** */

31

/**************************************************************/

32

33

34

/* $RCSfile: eml.c,v $ */

35

36

#include "cnf.h"

37

#include "eml.h"

38

#include "foldfg.h"

39

#include "flags.h"

40

41

SYMBOL eml_APPLYF;

42

SYMBOL eml_BOX;

43

SYMBOL eml_COMP;

44

SYMBOL eml_CONV;

45

SYMBOL eml_DIA;

46

SYMBOL eml_DIV;

47

SYMBOL eml_DOMAIN;

48

SYMBOL eml_DOMRESTR;

49

SYMBOL eml_ID;

50

SYMBOL eml_RANGE;

51

SYMBOL eml_RANRESTR;

52

SYMBOL eml_SUM;

53

SYMBOL eml_TEST;

54

55

LIST eml_SYMBOLS; /* eml junctor symbols */

56

57

LIST *eml_PROPINDEXTOFOSYMBOL; /* list of FO symbols associated with

58

eml prop/junctor symbols */

59

SYMBOL eml_SEMIFNDESYMBOLS[symbol__MAXSIGNATURE];

60

/* nde symbols associated with diamonds */

61

SYMBOL eml_NARYSYMBOLS[symbol__MAXSIGNATURE][eml__MAXMODALDEPTH];

62

/* FO symbols with particular

63

* arity associated with p's */

64

65

static const char* eml_PREDNAMEPREFIX[6] = { "SkQ", "SkR", "SkNde" , "SkQ", "SkNde", "SkS" };

66

67

static const char* eml_RELPROPERTYLABELS[6] = { "", "serial",

68

"reflexive" , "symmetric", "transitive", "euclidean" };

69

70

static TERM eml_RemoveTrivialAtomsAndOps(TERM);

71

static TERM eml_RemoveTrivialOperator(TERM Term);

72

73

static TERM eml_EmbedInRelCalculusProp(TERM);

74

static TERM eml_EmbedInRelCalculusRel(TERM);

75

76

static TERM eml_RelationalTranslationProp(TERM, SYMBOL, FLAGSTORE, PRECEDENCE);

77

static TERM eml_RelationalTranslationRel(TERM, SYMBOL, SYMBOL, FLAGSTORE, PRECEDENCE);

78

79

static TERM eml_FunctTranslProp(TERM, TERM, FLAGSTORE, PRECEDENCE);

80

static TERM eml_FunctTranslRel(TERM, TERM, FLAGSTORE, PRECEDENCE);

81

static TERM eml_FunctTranslItoNaryPredProp(TERM, LIST, char*, int, FLAGSTORE, PRECEDENCE);

82

static TERM eml_FunctTranslItoNaryPredRel(TERM, LIST, char*, int, FLAGSTORE, PRECEDENCE);

83

84

static TERM eml_SemiFunctTranslProp(TERM, TERM, int, FLAGSTORE, PRECEDENCE);

85

static TERM eml_SemiFunctTranslRelBox(TERM, TERM, TERM, FLAGSTORE, PRECEDENCE);

86

static TERM eml_SemiFunctTranslRelDia(TERM, TERM, FLAGSTORE, PRECEDENCE);

87

88

static TERM eml_RelFunctTranslProp(TERM, SYMBOL, char*, FLAGSTORE, PRECEDENCE);

89

static TERM eml_RelFunctTranslRel(TERM, SYMBOL, SYMBOL, char*, FLAGSTORE, PRECEDENCE);

90

91

/**************************************************************/

92

/* ********************************************************** */

93

/* * * */

94

/* * FUNCTIONS * */

95

/* * * */

96

/* ********************************************************** */

97

/**************************************************************/

98

99

void eml_Init(PRECEDENCE Precedence)

100

/**************************************************************

101

INPUT: None.

102

RETURNS: None.

103

USAGE: extern public.

104

SUMMARY: Initializes the Eml Module.

105

EFFECTS: All additional extended modal logic symbols are created.

106

(The first-order symbols are created in fol_Init.)

107

And, creates an array for the list of

108

propositional/first-order symbol pairs as well as Eml logical

109

symbols/first-order logical symbol lists.

110

CAUTION: MUST BE CALLED BEFORE ANY OTHER eml-FUNCTION.

111

***************************************************************/

112

{

113

int i;

114

115

eml_BOX = symbol_CreateJunctor("box", 2, symbol_STATLEX, Precedence);

116

eml_COMP = symbol_CreateJunctor("comp", 2, symbol_STATLEX, Precedence);

117

eml_CONV = symbol_CreateJunctor("conv", 1, symbol_STATLEX, Precedence);

118

eml_DIA = symbol_CreateJunctor("dia", 2, symbol_STATLEX, Precedence);

119

eml_DIV = symbol_CreatePredicate("div", 0, symbol_STATLEX, Precedence);

120

eml_DOMAIN = symbol_CreateJunctor("domain", 1, symbol_STATLEX, Precedence);

121

eml_DOMRESTR = symbol_CreateJunctor("domrestr", 2, symbol_STATLEX, Precedence);

122

eml_ID = symbol_CreatePredicate("id", 0, symbol_STATLEX, Precedence);

123

eml_RANGE = symbol_CreateJunctor("range", 1, symbol_STATLEX, Precedence);

124

eml_RANRESTR = symbol_CreateJunctor("ranrestr", 2, symbol_STATLEX, Precedence);

125

eml_SUM = symbol_CreateJunctor("sum", 2, symbol_STATLEX, Precedence);

126

eml_TEST = symbol_CreateJunctor("test", 1, symbol_STATLEX, Precedence);

127

symbol_AddProperty(eml_DIV, PREDEFINED);

128

symbol_AddProperty(eml_ID, PREDEFINED);

129

130

eml_SYMBOLS =

131

list_Cons((POINTER)eml_BOX, list_Cons((POINTER)eml_COMP,

132

list_Cons((POINTER)eml_CONV, list_Cons((POINTER)eml_DIA,

133

list_Cons((POINTER)eml_DIV, list_Cons((POINTER)eml_DOMAIN,

134

list_Cons((POINTER)eml_DOMRESTR, list_Cons((POINTER)eml_ID,

135

list_Cons((POINTER)eml_RANGE, list_Cons((POINTER)eml_RANRESTR,

136

list_Cons((POINTER)eml_SUM, list_List((POINTER)eml_TEST))))))))))));

137

138

eml_PROPINDEXTOFOSYMBOL = (LIST*)memory_Malloc(sizeof(LIST) * symbol__MAXSIGNATURE);

139

for (i=0;i< symbol__MAXSIGNATURE;i++)

140

eml_PROPINDEXTOFOSYMBOL[i] = list_Nil();

141

142

eml_SetPropFoSymbolAssocList(eml_Dia(),

143

list_Cons((POINTER)fol_Exist(), list_List((POINTER)fol_And())));

144

eml_SetPropFoSymbolAssocList(eml_Box(),

145

list_Cons((POINTER)fol_All(), list_List((POINTER)fol_Implies())));

146

eml_SetPropFoSymbolAssocList(eml_Comp(),

147

list_Cons((POINTER)fol_Exist(), list_List((POINTER)fol_And())));

148

eml_SetPropFoSymbolAssocList(eml_Sum(),

149

list_Cons((POINTER)fol_All(), list_List((POINTER)fol_Or())));

150

eml_SetPropFoSymbolAssocList(eml_Domain(),

151

list_List((POINTER)fol_Exist()));

152

eml_SetPropFoSymbolAssocList(eml_Range(),

153

list_List((POINTER)fol_Exist()));

154

eml_SetPropFoSymbolAssocList(eml_Id(),

155

list_List((POINTER)fol_Equality()));

156

}

157

158

BOOL eml_FormulaContainsEMLTheorySymbol(TERM Formula)

159

/**************************************************************

160

INPUT: A term or a formula

161

RETURNS: TRUE iff <Formula> contains an EML theory symbol.

162

USAGE: extern public.

163

***************************************************************/

164

{

165

SYMBOL Top;

166

LIST Scan;

167

168

Top = term_TopSymbol(Formula);

169

170

if (symbol_IsPredicate(Top)) {

171

if (symbol_Equal(eml_DIV,Top) || symbol_Equal(eml_ID,Top))

172

return TRUE;

173

else

174

return FALSE;

175

}

176

if (symbol_IsFunction(Top) || symbol_IsVariable(Top))

177

return FALSE;

178

179

if (symbol_Equal(Top, eml_BOX) || symbol_Equal(Top, eml_COMP) || symbol_Equal(Top, eml_CONV) ||

180

symbol_Equal(Top, eml_SUM) || symbol_Equal(Top, eml_DIV) || symbol_Equal(Top, eml_DOMAIN) ||

181

symbol_Equal(Top, eml_DOMRESTR) || symbol_Equal(Top, eml_RANGE) || symbol_Equal(Top, eml_RANRESTR) ||

182

symbol_Equal(Top, eml_TEST))

183

return TRUE;

184

185

if (fol_IsQuantifier(Top))

186

Scan = list_Cdr(term_ArgumentList(Formula));

187

else

188

Scan = term_ArgumentList(Formula);

189

190

while (!list_Empty(Scan)) {

191

if (eml_FormulaContainsEMLTheorySymbol((TERM)list_First(Scan)))

192

return TRUE;

193

Scan = list_Cdr(Scan);

194

}

195

196

return FALSE;

197

198

}

199

200

void eml_InitFunctTransl(FLAGSTORE Flags, PRECEDENCE Precedence)

201

/**************************************************************

202

INPUT: None.

203

RETURNS: None.

204

USAGE: static intern.

205

SUMMARY: Initializes the routines for the functional translation of

206

basic (serial) modal logics ito n-ary predicates.

207

EFFECTS: Additonal flags are set.

208

CAUTION: Prerequisite for the functional translation ito n-ary predicates

209

routines.

210

***************************************************************/

211

{

212

/* printf("\nDoing eml_InitFunctTransl()\n"); */

213

214

/* Dynamic memory allocation of eml_NARYSYMBOLS??

215

* This does not work:

216

eml_NARYSYMBOLS = (SYMBOL **)memory_Malloc(sizeof(SYMBOL) * symbol__MAXSIGNATURE *

217

symbol__MAXSIGNATURE);

218

*/

219

if ( (flag_GetFlagIntValue(Flags, flag_EMLTR) == flag_EMLTRSEMIFUNC) ||

220

!flag_GetFlagIntValue(Flags, flag_EMLFNARY)) {

221

eml_APPLYF = symbol_CreateFunction("app", 2, symbol_STATLEX, Precedence);

222

/* fol_SYMBOLS = list_Cons((POINTER)eml_APPLYF, fol_SYMBOLS);*/

223

}

224

225

}

226

227

228

void eml_Free(void)

229

/**************************************************************

230

INPUT: None.

231

RETURNS: void.

232

EFFECT: The eml related memory used by the eml module is freed.

233

***************************************************************/

234

{

235

int i;

236

237

list_Delete(eml_SYMBOLS);

238

239

for (i=0;i< symbol__MAXSIGNATURE;i++)

240

list_Delete(eml_PROPINDEXTOFOSYMBOL[i]);

241

242

memory_Free(eml_PROPINDEXTOFOSYMBOL, sizeof(LIST) * symbol__MAXSIGNATURE);

243

244

/* list_Delete(eml_NARYSYMBOLS); ?? */

245

}

246

247

LIST eml_NullaryPredList()

248

/**************************************************************

249

INPUT: None.

250

RETURNS: The list of nullary predicate symbols in the signature

251

USAGE: not used.

252

EFFECTS: Creates a table for the list of

253

propositional/first-order symbol pairs.

254

***************************************************************/

255

{

256

LIST nullaryPredList;

257

int i;

258

259

if (!symbol_SignatureExists()) {

260

fprintf(stderr,"\n\t eml_NullaryPredList(): no signature!?\n");

261

misc_Error();

262

}

263

264

nullaryPredList = list_Nil();

265

for(i = 1; i < symbol_ACTINDEX; i++)

266

if (!symbol_IsFreed(i) &&

267

eml_IsNullaryPredicate(symbol_GetSigSymbol(i)))

268

nullaryPredList =

269

list_Cons((POINTER)(symbol_GetSigSymbol(i)),

270

nullaryPredList);

271

272

#ifdef DEBUG

273

printf("\n nullaryPredList: ");

274

for (Scan=nullaryPredList; !list_Empty(Scan); Scan=list_Cdr(Scan)) {

275

symbol_Print((SYMBOL)list_Car(Scan));

276

printf(" ");

277

}

278

printf("\n");

279

#endif

280

281

return nullaryPredList;

282

}

283

284

static SYMBOL eml_GetFoSymbolAssocWithPropSymbol(SYMBOL

285

PropSymbol, NAT Arity, eml_SYMBOLTYPE SymbolType)

286

/**************************************************************

287

INPUT: a (propositional) symbol, the arity of the corresponding

288

predicate symbol, the symbol type.

289

RETURNS: The corresponding first-order symbol.

290

EFFECTS: None.

291

***************************************************************/

292

{

293

/* printf("\n PropSymbol = "); */

294

/* symbol_Print(PropSymbol); */

295

if (eml_NaryType(SymbolType)) {

296

/* Retrieve symbol with given arity */

297

SYMBOL symbol;

298

/* printf("\n eml_NaryType"); */

299

symbol = eml_NARYSYMBOLS[symbol_Index(PropSymbol)][Arity-1];

300

if (symbol_IsSymbol(symbol))

301

return symbol;

302

}

303

else if (eml_SemiFuncNdeType(SymbolType)) {

304

/* Retrieve nde symbol for semi-functional translation */

305

SYMBOL symbol;

306

/* printf("\n eml_SemiFuncNdeType"); */

307

symbol = eml_SEMIFNDESYMBOLS[symbol_Index(PropSymbol)];

308

if (symbol_IsSymbol(symbol))

309

return symbol;

310

}

311

else if (eml_VarSortType(SymbolType)) {

312

/* Reuse propositional symbol as predicate symbol to indicate the

313

* sort */

314

/* printf("\n eml_VarSortType"); */

315

return PropSymbol; /* Struture sharing!

316

* Alternatively, set up another array called

317

* eml_PROPINDEXTOSORTSYMBOL, say */

318

}

319

else {

320

/* Retrieve predicate symbol: P_p for p, and R_r for r */

321

LIST symbolList;

322

/* printf("\n not eml_NaryType and not eml_VarSortType"); */

323

symbolList = eml_PROPINDEXTOFOSYMBOL[symbol_Index(PropSymbol)];

324

if (!list_Empty(symbolList))

325

return (SYMBOL) list_First(symbolList);

326

}

327

328

/* printf("\n not eml_NaryType and not eml_VarSortType and symbolList is empty"); */

329

return symbol__NULL;

330

}

331

332

333

SYMBOL eml_CreateFoSymbol(SYMBOL PropSymbol, eml_SYMBOLTYPE SymbolType,

334

int Arity, int Status, PRECEDENCE Precedence)

335

/*******************************************************

336

INPUT: A symbol (which MUST be a propositonal symbol/nullary

337

predicate symbol), a symbol type (of the fo symbol to be

338

created), the arity of the new symbol, The status of the new

339

symbol.

340

RETURNS: A first-order symbol corresponding to PropSymbol.

341

********************************************************/

342

{

343

SYMBOL foSymbol;

344

int size;

345

char* newName;

346

347

if (eml_NaryType(SymbolType)) {

348

char* arityStr = string_IntToString(Arity);

349

size = strlen(eml_PREDNAMEPREFIX[SymbolType])+strlen(arityStr)+strlen(symbol_Name(PropSymbol))+1;

350

newName = memory_Malloc(size*sizeof(char));

351

352

/* Note: if SymbolType is n-ary then any propositional symbol can

353

* be associated with more than one n-ary predicate symbol, for

354

* that reason no user defined FoSymbols will be considered */

355

sprintf(newName,"%s%s%s", eml_PREDNAMEPREFIX[SymbolType], arityStr,

356

symbol_Name(PropSymbol));

357

foSymbol = symbol_CreatePredicate(newName, Arity, Status, Precedence);

358

eml_SetPropNarySymbolAssocList(PropSymbol, Arity, foSymbol);

359

360

memory_Free(newName,size*sizeof(char));

361

string_StringFree(arityStr);

362

}

363

else if (eml_SemiFuncNdeType(SymbolType)) {

364

size = strlen(eml_PREDNAMEPREFIX[eml_NDE])+strlen(symbol_Name(PropSymbol))+1;

365

newName = memory_Malloc(size*sizeof(char));

366

367

/* NOTE: For the moment no user defined FoSymbols will be

368

* considered. This restriction is provisional */

369

sprintf(newName,"%s%s", eml_PREDNAMEPREFIX[eml_NDE],

370

symbol_Name(PropSymbol));

371

foSymbol = symbol_CreatePredicate(newName, Arity, Status, Precedence);

372

eml_SetPropSemiFNdeSymbolAssocList(PropSymbol, Arity, foSymbol);

373

374

memory_Free(newName,size*sizeof(char));

375

}

376

else {

377

size = strlen(eml_PREDNAMEPREFIX[SymbolType])+strlen(symbol_Name(PropSymbol))+1;

378

newName = memory_Malloc(size*sizeof(char));

379

380

sprintf(newName,"%s%s", eml_PREDNAMEPREFIX[SymbolType],

381

symbol_Name(PropSymbol));

382

foSymbol = symbol_CreatePredicate(newName, Arity, Status, Precedence);

383

eml_SetPropFoSymbolAssocList(PropSymbol,list_List((POINTER)foSymbol));

384

385

memory_Free(newName,size*sizeof(char));

386

}

387

388

return foSymbol;

389

}

390

391

TERM eml_CreateQuantifier(TERM Term, SYMBOL Quantifier, LIST VarList,

392

LIST Arguments)

393

/*******************************************************

394

INPUT: A term (dummy, not used), symbol (which MUST be a fol

395

quantifier), a list of variables that will be bound, and

396

a list of arguments.

397

RETURNS: A new quantified term.

398

********************************************************/

399

{

400

return term_Create(Quantifier,

401

list_Cons(term_Create(fol_Varlist(), VarList),

402

Arguments));

403

}

404

405

static TERM eml_RplacWithQuantifier(TERM Term, SYMBOL Quantifier,

406

LIST VarList, LIST Arguments)

407

/**************************************************************

408

INPUT: A formula, a symbol (quantifier), two list of terms.

409

RETURNS: A quantifier replacement.

410

EFFECT: Note, a term node is created for the variable list.

411

CAUTION: The term in destructively changed.

412

***************************************************************/

413

{

414

term_RplacTop(Term,Quantifier);

415

term_RplacArgumentList(Term,

416

list_Cons(term_Create(fol_Varlist(), VarList), Arguments));

417

418

return Term;

419

}

420

421

static TERM eml_BuildSortQuantifierFor(TERM Term, SYMBOL ModalTop,

422

SYMBOL RelSubTop, SYMBOL Var, BOOL WithSort,

423

LIST Arguments, POINTER (*BuildFunction)(),

424

PRECEDENCE Precedence)

425

/*******************************************************

426

INPUT: A term (which MUST be a modal term, i.e. dia(..) or box (...)),

427

a single variable, a Boolean value indicating whether sorts or

428

required, and a list of arguments.

429

RETURNS: A quantified term, possibly restricted by the appropriate sort.

430

CAUTION: The term is potentially destructively changed (depends on the

431

BuildFunction).

432

********************************************************/

433

{

434

#ifdef DEBUG

435

if (!eml_IsModalOpSymbol(ModalTop)) {

436

printf("\n\nIllegal input in eml_BuildSortQuantifierFor\n");

437

misc_Error();

438

}

439

#endif

440

441

if (WithSort) {

442

eml_SYMBOLTYPE symbolType;

443

SYMBOL foSymbol;

444

#ifdef DEBUG

445

if (!eml_IsNullaryPredicate(RelSubTop)) {

446

printf("\n\nIllegal relational argument of modal operator, in eml_BuildSortQuantifierFor\n");

447

misc_Error();

448

}

449

#endif

450

451

symbolType = eml_VARSORT;

452

foSymbol = eml_GetFoSymbolAssocWithPropSymbol(RelSubTop, 1, symbolType);

453

if (foSymbol == symbol__NULL) {

454

foSymbol = eml_CreateFoSymbol(RelSubTop, symbolType, 1, symbol_STATLEX, Precedence);

455

/* Inheritance of precedence? */

456

/* symbol_SetOrdering(Precedence, foSymbol,symbol_Ordering(Precedence, PropSymbol)); */

457

}

458

return BuildFunction(Term, eml_FoQuantAssocWithPropSymbol(ModalTop),

459

list_List(term_Create(Var,list_Nil())),

460

list_List(term_Create(eml_FoJunctorAssocWithPropSymbol(ModalTop),

461

list_Cons(term_Create(foSymbol,list_List(term_Create(Var,list_Nil()))), Arguments))));

462

/* exists x S(x) /\ ...

463

* forall x S(x) -> ... */

464

}

465

else {

466

return BuildFunction(Term, eml_FoQuantAssocWithPropSymbol(ModalTop),

467

list_List(term_Create(Var,list_Nil())), Arguments);

468

/* exists x ...

469

* forall x ... */

470

}

471

}

472

473

static TERM eml_RplacWithDesignatedPropAtom(TERM Term, SYMBOL RplacSymbol)

474

/**************************************************************

475

INPUT: A formula and a symbol.

476

RETURNS: A replacement without arguments, e.g. true, false, id, etc.

477

CAUTION: The term in destructively changed.

478

***************************************************************/

479

{

480

term_RplacTop(Term,RplacSymbol);

481

list_DeleteWithElement(term_ArgumentList(Term),(void (*)())term_Delete);

482

term_RplacArgumentList(Term,list_Nil());

483

484

return Term;

485

}

486

487

static TERM eml_RplacWithOpAndArgs(TERM Term, SYMBOL RplacSymbol,

488

LIST Arguments)

489

/**************************************************************

490

INPUT: A formula, a symbol and a list of terms.

491

RETURNS: A replacement with argument list.

492

CAUTION: The term in destructively changed.

493

***************************************************************/

494

{

495

term_RplacTop(Term,RplacSymbol);

496

term_RplacArgumentList(Term,Arguments);

497

498

return Term;

499

}

500

501

static TERM eml_RemoveTrivialOperator(TERM Term)

502

/**************************************************************

503

INPUT: A formula.

504

RETURNS: The formula after

505

removal of "or", "and", "comp" and "sum" with only one argument

506

CAUTION: The term in destrucively changed.

507

***************************************************************/

508

{

509

if (eml_IsNaryJunctor(term_TopSymbol(Term)) &&

510

list_Empty(list_Cdr(term_ArgumentList(Term)))) {

511

TERM helpTerm = term_FirstArgument(Term);

512

list_Delete(term_ArgumentList(Term));

513

Term = eml_RplacWithOpAndArgs(Term, term_TopSymbol(helpTerm), term_ArgumentList(helpTerm));

514

term_Free(helpTerm);

515

}

516

517

return Term;

518

}

519

520

static TERM eml_RemoveTrivialAtomsAndOps(TERM Term)

521

/**************************************************************

522

INPUT: A formula.

523

RETURNS: The formula after applying

524

or(true,...) -> true, and(true,phi) -> phi

525

or(false,phi) -> phi, and(false,...) -> false

526

etc plus

527

dia(alpha,false) -> false, box(alpha,true) -> true

528

dia(false,phi) -> false, box(false,phi) -> true

529

CAUTION: The term in destructively changed.

530

***************************************************************/

531

{

532

SYMBOL Top, Subtop, RelSubtop;

533

LIST Scan;

534

TERM Subterm, RelSubterm;

535

BOOL Update;

536

537

if (!term_IsComplex(Term))

538

return Term;

539

540

Top = term_TopSymbol(Term);

541

Update = FALSE;

542

543

/* Term = and(...) */

544

if (symbol_Equal(Top,fol_And())) {

545

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) {

546

Subterm = eml_RemoveTrivialAtomsAndOps(list_Car(Scan));

547

Subtop = term_TopSymbol(Subterm);

548

if (symbol_Equal(Subtop,fol_True()))

549

Update = TRUE;

550

else if (symbol_Equal(Subtop,fol_False())) {

551

/* and(..., false, ...) -> false */

552

return eml_RplacWithDesignatedPropAtom(Term,fol_False());

553

}

554

}

555

if (Update) {

556

/* and(..., true, ..., true, ...) -> and(..., ..., ...) */

557

term_RplacArgumentList(Term,list_DeleteElementIfFree(term_ArgumentList(Term),(BOOL (*)())fol_IsTrue,(void (*)())term_Delete));

558

if (list_Empty(term_ArgumentList(Term))) {

559

term_RplacTop(Term,fol_True());

560

return Term;

561

}

562

}

563

return eml_RemoveTrivialOperator(Term); /* and(phi) -> phi */

564

}

565

/* Term = or(...) */

566

else if (symbol_Equal(Top,fol_Or())) {

567

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) {

568

Subterm = eml_RemoveTrivialAtomsAndOps(list_Car(Scan));

569

Subtop = term_TopSymbol(Subterm);

570

if (symbol_Equal(Subtop,fol_False()))

571

Update = TRUE;

572

else if (symbol_Equal(Subtop,fol_True())) {

573

/* or(..., true, ...) -> true */

574

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

575

}

576

}

577

if (Update) {

578

term_RplacArgumentList(Term,list_DeleteElementIfFree(term_ArgumentList(Term),(BOOL (*)())fol_IsFalse,(void (*)())term_Delete));

579

if (list_Empty(term_ArgumentList(Term))) {

580

term_RplacTop(Term,fol_False());

581

return Term;

582

}

583

}

584

return eml_RemoveTrivialOperator(Term); /* or(phi) -> phi */

585

}

586

/* Term = not(...) */

587

else if (symbol_Equal(Top,fol_Not())) {

588

Subterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

589

Subtop = term_TopSymbol(Subterm);

590

if (eml_IsDesignatedPropSymbol(Subtop)) {

591

/* not(false) -> true, not(true) -> false, not(div) -> id, not(id) -> div */

592

return eml_RplacWithDesignatedPropAtom(Term,eml_GetDualSymbol(Subtop));

593

}

594

}

595

/* Term = forall(...) or Term = exists(...) */

596

else if (fol_IsQuantifier(Top)) {

597

Subterm = eml_RemoveTrivialAtomsAndOps(term_SecondArgument(Term));

598

Subtop = term_TopSymbol(Subterm);

599

if (symbol_Equal(Subtop,fol_True())) {

600

/* forall ... true -> true, exists ... true -> true */

601

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

602

}

603

else if (symbol_Equal(Subtop,fol_False())) {

604

/* forall ... false -> false, exists ... false -> false */

605

return eml_RplacWithDesignatedPropAtom(Term,fol_False());

606

}

607

}

608

/* Term = dia(...) or Term = box(...) */

609

else if (eml_IsModalOpSymbol(Top)) {

610

RelSubterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

611

RelSubtop = term_TopSymbol(RelSubterm);

612

Subterm = eml_RemoveTrivialAtomsAndOps(term_SecondArgument(Term));

613

Subtop = term_TopSymbol(Subterm);

614

if (symbol_Equal(Top,eml_Dia()) &&

615

(symbol_Equal(Subtop,fol_False()) || symbol_Equal(RelSubtop,fol_False()))) {

616

/* dia(alpha,false) -> false, dia(false,phi) -> false */

617

return eml_RplacWithDesignatedPropAtom(Term,fol_False());

618

}

619

else if (symbol_Equal(Top,eml_Box()) &&

620

(symbol_Equal(Subtop,fol_True()) || symbol_Equal(RelSubtop,fol_False()))) {

621

/* box(alpha,true) -> true, box(true,phi) -> true */

622

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

623

}

624

else if (symbol_Equal(RelSubtop, eml_Id())) {

625

/* dia(id,phi) -> phi, box(id,phi) -> phi */

626

term_Delete(RelSubterm);

627

list_Delete(term_ArgumentList(Term));

628

Term = eml_RplacWithOpAndArgs(Term, Subtop, term_ArgumentList(Subterm));

629

term_Free(Subterm);

630

return Term;

631

}

632

}

633

/* Term = domain(...) or Term = range(...) */

634

else if (symbol_Equal(Top,eml_Domain()) || symbol_Equal(Top,eml_Range())) {

635

RelSubterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

636

RelSubtop = term_TopSymbol(RelSubterm);

637

if (symbol_Equal(RelSubtop,fol_False())) {

638

/* domain(false) -> false, range(false) -> false */

639

return eml_RplacWithDesignatedPropAtom(Term,fol_False());

640

}

641

else if (symbol_Equal(RelSubtop, eml_Id())) {

642

/* domain(id) -> true, range(id) -> true */

643

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

644

}

645

}

646

/* Term = implies(...) */

647

else if (symbol_Equal(Top,fol_Implies())) {

648

Subterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

649

Subtop = term_TopSymbol(Subterm);

650

if (symbol_Equal(Subtop,fol_False())) {

651

/* implies(false,phi) -> true */

652

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

653

}

654

else if (symbol_Equal(Subtop,fol_True())) {

655

/* implies(true,phi) -> phi */

656

term_Delete(Subterm);

657

Subterm = term_SecondArgument(Term);

658

list_Delete(term_ArgumentList(Term));

659

Term = eml_RplacWithOpAndArgs(Term,term_TopSymbol(Subterm),term_ArgumentList(Subterm));

660

term_Free(Subterm);

661

return eml_RemoveTrivialAtomsAndOps(Term);

662

}

663

Subterm = eml_RemoveTrivialAtomsAndOps(term_SecondArgument(Term));

664

Subtop = term_TopSymbol(Subterm);

665

if (symbol_Equal(Subtop,fol_True())) {

666

/* implies(phi,true) -> true */

667

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

668

}

669

else if (symbol_Equal(Subtop,fol_False())) {

670

/* implies(phi,false) -> not(phi) */

671

Term = eml_RplacWithOpAndArgs(Term, fol_Not(),

672

list_DeleteElementIfFree(term_ArgumentList(Term),

673

(BOOL (*)())fol_IsFalse, (void (*)())term_Delete));

674

return eml_RemoveTrivialAtomsAndOps(Term);

675

}

676

}

677

/* Term = implied(...) */

678

else if (symbol_Equal(Top,fol_Implied())) {

679

Subterm = eml_RemoveTrivialAtomsAndOps(term_SecondArgument(Term));

680

Subtop = term_TopSymbol(Subterm);

681

if (symbol_Equal(Subtop,fol_False())) {

682

/* implied(phi,false) -> true */

683

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

684

}

685

else if (symbol_Equal(Subtop,fol_True())) {

686

/* implied(phi,true) -> phi */

687

term_Delete(Subterm);

688

Subterm = term_FirstArgument(Term);

689

list_Delete(term_ArgumentList(Term));

690

Term = eml_RplacWithOpAndArgs(Term,term_TopSymbol(Subterm),term_ArgumentList(Subterm));

691

term_Free(Subterm);

692

return eml_RemoveTrivialAtomsAndOps(Term);

693

}

694

Subterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

695

Subtop = term_TopSymbol(Subterm);

696

if (symbol_Equal(Subtop,fol_True()))

697

/* implied(true,phi) -> true */

698

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

699

else if (symbol_Equal(Subtop,fol_False())) {

700

/* implied(false,phi) -> not(phi) */

701

Term = eml_RplacWithOpAndArgs(Term, fol_Not(),

702

list_DeleteElementIfFree(term_ArgumentList(Term),

703

(BOOL (*)())fol_IsFalse, (void (*)())term_Delete));

704

return eml_RemoveTrivialAtomsAndOps(Term);

705

}

706

}

707

/* Term = equiv(...) */

708

else if (symbol_Equal(Top,fol_Equiv())) {

709

Subterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

710

Subtop = term_TopSymbol(Subterm);

711

if (symbol_Equal(Subtop,fol_False())) {

712

/* equiv(false,phi) -> not(phi) */

713

Term = eml_RplacWithOpAndArgs(Term, fol_Not(),

714

list_DeleteElementIfFree(term_ArgumentList(Term),

715

(BOOL (*)())fol_IsFalse, (void (*)())term_Delete));

716

return eml_RemoveTrivialAtomsAndOps(Term);

717

}

718

else if (symbol_Equal(Subtop,fol_True())) {

719

/* equiv(true,phi) -> phi */

720

term_Delete(Subterm);

721

Subterm = term_SecondArgument(Term);

722

list_Delete(term_ArgumentList(Term));

723

Term = eml_RplacWithOpAndArgs(Term, term_TopSymbol(Subterm),

724

term_ArgumentList(Subterm));

725

term_Free(Subterm);

726

return eml_RemoveTrivialAtomsAndOps(Term);

727

}

728

Subterm = eml_RemoveTrivialAtomsAndOps(term_SecondArgument(Term));

729

Subtop = term_TopSymbol(Subterm);

730

if (symbol_Equal(Subtop,fol_False())) {

731

/* equiv(phi,false) -> not(phi) */

732

Term = eml_RplacWithOpAndArgs(Term, fol_Not(),

733

list_DeleteElementIfFree(term_ArgumentList(Term),

734

(BOOL (*)())fol_IsFalse, (void (*)())term_Delete));

735

return eml_RemoveTrivialAtomsAndOps(Term);

736

}

737

else if (symbol_Equal(Subtop,fol_True())) {

738

/* equiv(phi,true) -> phi */

739

term_Delete(Subterm);

740

Subterm = term_FirstArgument(Term);

741

list_Delete(term_ArgumentList(Term));

742

Term = eml_RplacWithOpAndArgs(Term, term_TopSymbol(Subterm),

743

term_ArgumentList(Subterm));

744

term_Free(Subterm);

745

}

746

}

747

/* Term = comp(...) */

748

else if (symbol_Equal(Top,eml_Comp())) {

749

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) {

750

Subterm = eml_RemoveTrivialAtomsAndOps(list_Car(Scan));

751

Subtop = term_TopSymbol(Subterm);

752

if (symbol_Equal(Subtop,eml_Id()))

753

Update = TRUE;

754

else if (symbol_Equal(Subtop,fol_False())) {

755

/* comp(..., false, ...) -> false */

756

return eml_RplacWithDesignatedPropAtom(Term,fol_False());

757

}

758

}

759

if (Update) {

760

/* comp(..., id, ..., id, ...) -> comp(..., ..., ...) */

761

term_RplacArgumentList(Term,

762

list_DeleteElementIfFree(term_ArgumentList(Term),

763

(BOOL (*)())eml_IsId, (void (*)())term_Delete));

764

if (list_Empty(term_ArgumentList(Term))) {

765

term_RplacTop(Term,eml_Id());

766

return Term;

767

}

768

}

769

return eml_RemoveTrivialOperator(Term); /* comp(alpha) -> alpha */

770

}

771

/* Term = sum(...) */

772

else if (symbol_Equal(Top,eml_Sum())) {

773

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan)) {

774

Subterm = eml_RemoveTrivialAtomsAndOps(list_Car(Scan));

775

Subtop = term_TopSymbol(Subterm);

776

if (symbol_Equal(Subtop,eml_Div()))

777

Update = TRUE;

778

else if (symbol_Equal(Subtop,fol_True())) {

779

/* sum(..., true, ...) -> true */

780

return eml_RplacWithDesignatedPropAtom(Term,fol_True());

781

}

782

}

783

if (Update) {

784

/* sum(..., div, ..., div, ...) -> sum(..., ..., ...) */

785

term_RplacArgumentList(Term,

786

list_DeleteElementIfFree(term_ArgumentList(Term),

787

(BOOL (*)())eml_IsDiv, (void (*)())term_Delete));

788

if (list_Empty(term_ArgumentList(Term))) {

789

term_RplacTop(Term,eml_Div());

790

return Term;

791

}

792

}

793

return eml_RemoveTrivialOperator(Term); /* sum(alpha) -> alpha */

794

}

795

/* Term = test(...) */

796

else if (symbol_Equal(Top,eml_Test())) {

797

Subterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

798

Subtop = term_TopSymbol(Subterm);

799

if (symbol_Equal(Subtop,fol_False())) {

800

/* test(false) -> false */

801

return eml_RplacWithDesignatedPropAtom(Term,fol_False());

802

}

803

else if (symbol_Equal(Subtop, fol_True())) {

804

/* test(true) -> id */

805

return eml_RplacWithDesignatedPropAtom(Term,eml_Id());

806

}

807

}

808

/* Term = conv(...) */

809

else if (symbol_Equal(Top,eml_Conv())) {

810

RelSubterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

811

RelSubtop = term_TopSymbol(RelSubterm);

812

if (symbol_Equal(RelSubtop,fol_True()) ||

813

symbol_Equal(RelSubtop,fol_False()) ||

814

symbol_Equal(RelSubtop,eml_Id()) ||

815

symbol_Equal(RelSubtop,eml_Div())) {

816

/* conv(false) -> false, conv(true) -> true, conv(id) -> id, conv(div) -> div */

817

return eml_RplacWithDesignatedPropAtom(Term,RelSubtop);

818

}

819

else if (symbol_Equal(RelSubtop,eml_Test())) {

820

/* conv(test(...)) -> test(...) */

821

list_Delete(term_ArgumentList(Term));

822

Term = eml_RplacWithOpAndArgs(Term, RelSubtop, term_ArgumentList(RelSubterm));

823

term_Free(RelSubterm);

824

return Term;

825

}

826

}

827

/* Term = domrestr(...) or Term = ranrestr(...) */

828

else if (symbol_Equal(Top,eml_DomRestr()) || symbol_Equal(Top,eml_RanRestr())) {

829

RelSubterm = eml_RemoveTrivialAtomsAndOps(term_FirstArgument(Term));

830

RelSubtop = term_TopSymbol(RelSubterm);

831

Subterm = eml_RemoveTrivialAtomsAndOps(term_SecondArgument(Term));

832

Subtop = term_TopSymbol(Subterm);

833

if (symbol_Equal(RelSubtop,fol_False()) || symbol_Equal(Subtop,fol_False())) {

834

/* domrestr(false,...), domrestr(...,false) -> false,

835

* ranrestr(false,...), ranrestr(...,false) -> false */

836

return eml_RplacWithDesignatedPropAtom(Term,fol_False());

837

}

838

else if (symbol_Equal(Subtop, fol_True())) {

839

/* domrestr(alpha,true) -> alpha, ranrestr(alpha,true) -> alpha */

840

term_Delete(Subterm);

841

list_Delete(term_ArgumentList(Term));

842

Term = eml_RplacWithOpAndArgs(Term, RelSubtop, term_ArgumentList(RelSubterm));

843

term_Free(RelSubterm);

844

return Term;

845

}

846

}

847

848

return Term;

849

}

850

851

static TERM eml_CreateModalTerm(SYMBOL ModOp, LIST RelTermList, TERM PropTerm)

852

/**************************************************************

853

INPUT: A symbol (either box or dia), a list of relational terms,

854

a list with one propositional term.

855

RETURNS: A nested box(..., box(..., box(..., ....)))

856

or dia(..., dia(..., dia(..., ....))) term

857

***************************************************************/

858

{

859

if (list_Empty(RelTermList)) {

860

return PropTerm;

861

}

862

else {

863

return term_Create(ModOp,

864

list_Cons(list_Car(RelTermList),

865

list_List(eml_CreateModalTerm(ModOp, list_Cdr(RelTermList), PropTerm))));

866

}

867

}

868

869

static TERM eml_EliminateComp(TERM Term)

870

/**************************************************************

871

INPUT: A Term.

872

RETURNS: eliminates comp if possible by replacing, e.g.

873

box(comp(..., ...., ....), ....) with

874

box(..., box(..., box(..., ....))).

875

CAUTION: The Term is destructively changed.

876

***************************************************************/

877

{

878

SYMBOL Top;

879

TERM RelSubterm;

880

881

Top = term_TopSymbol(Term);

882

883

/* box(comp(..., ...., ....), ....) -> box(..., box(..., box(..., ....)))

884

dia(comp(..., ...., ....), ....) -> dia(..., dia(..., dia(..., ....))) */

885

if (eml_IsModalOpSymbol(Top)) {

886

RelSubterm = term_FirstArgument(Term);

887

if (symbol_Equal(term_TopSymbol(RelSubterm),eml_Comp())) {

888

LIST ArgsList;

889

ArgsList = list_Cons(list_Car(term_ArgumentList(RelSubterm)),

890

list_List(eml_CreateModalTerm(Top,

891

list_Cdr(term_ArgumentList(RelSubterm)),

892

eml_EliminateComp(term_SecondArgument(Term)))));

893

list_Delete(term_ArgumentList(RelSubterm));

894

term_Free(RelSubterm);

895

list_Delete(term_ArgumentList(Term));

896

Term = eml_RplacWithOpAndArgs(Term, Top, ArgsList);

897

}

898

} else if (!symbol_IsPredicate(Top)) {

899

LIST Scan;

900

for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))

901

eml_EliminateComp(list_Car(Scan));

902

}

903

904

return Term;

905

}

906

907

static TERM eml_MakeOneAndOrCompSum(TERM Term)

908

/**************************************************************

909

INPUT: A Term.

910

RETURNS: Takes all arguments of an and together.

911

CAUTION: The Term is destructively changed.

912

***************************************************************/

913

{

914

SYMBOL Top;

915

LIST Scan;

916

TERM Subterm;

917

918

Top = term_TopSymbol(Term);

919

920

/* and(..., and( ..., ...)) -> and(..., ..., ...) */

921

if (symbol_Equal(Top,fol_And())) {

922

Scan = term_ArgumentList(Term);

923

while (!list_Empty(Scan)) {

924

Subterm = (TERM)list_Car(Scan);

925

eml_MakeOneAndOrCompSum(Subterm);

926

if (symbol_Equal(term_TopSymbol(Subterm),fol_And())) {

927

Scan = list_Cdr(Scan);

928

term_RplacArgumentList(Term,

929

list_Nconc(term_ArgumentList(Subterm),list_PointerDeleteElement(term_ArgumentList(Term),Subterm)));

930

term_Free(Subterm);

931

}

932

else

933

Scan = list_Cdr(Scan);

934

}

935

936

/* or(..., or( ..., ...)) -> or(..., ..., ...) */

937

} else if (symbol_Equal(Top,fol_Or())) {

938

Scan = term_ArgumentList(Term);

939

while (!list_Empty(Scan)) {

940

Subterm = (TERM)list_Car(Scan);

941

eml_MakeOneAndOrCompSum(Subterm);

942

if (symbol_Equal(term_TopSymbol(Subterm),fol_Or())) {

943

Scan = list_Cdr(Scan);

944

term_RplacArgumentList(Term,

945

list_Nconc(term_ArgumentList(Subterm),list_PointerDeleteElement(term_ArgumentList(Term),Subterm)));

946

term_Free(Subterm);

947

}

948

else

949

Scan = list_Cdr(Scan);

950

}

951

952

/* comp(..., comp( ..., ...)) -> comp(..., ..., ...) */

953

} else if (symbol_Equal(Top,eml_Comp())) {

954

Scan = term_ArgumentList(Term);

955

while (!list_Empty(Scan)) {

956

Subterm = (TERM)list_Car(Scan);

957

eml_MakeOneAndOrCompSum(Subterm);

958

if (symbol_Equal(term_TopSymbol(Subterm),eml_Comp())) {

959

Scan = list_Cdr(Scan);

960

term_RplacArgumentList(Term,

961

list_Nconc(term_ArgumentList(Subterm),list_PointerDeleteElement(term_ArgumentList(Term),Subterm)));

962

term_Free(Subterm);

963

}

964

else

965

Scan = list_Cdr(Scan);

966

}

967

968

/* sum(..., sum( ..., ...)) -> sum(..., ..., ...) */

969

} else if (symbol_Equal(Top,eml_Sum())) {

970

Scan = term_ArgumentList(Term);

971

while (!list_Empty(Scan)) {

972

Subterm = (TERM)list_Car(Scan);

973

eml_MakeOneAndOrCompSum(Subterm);

974

if (symbol_Equal(term_TopSymbol(Subterm),eml_Sum())) {

975

Scan = list_Cdr(Scan);

976

term_RplacArgumentList(Term,

977

list_Nconc(term_ArgumentList(Subterm),list_PointerDeleteElement(term_ArgumentList(Term),Subterm)));

978

term_Free(Subterm);

979

}

980

else

981

Scan = list_Cdr(Scan);

982

}

983

984

} else if (!symbol_IsPredicate(Top))

985

for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))

986

eml_MakeOneAndOrCompSum(list_Car(Scan));

987

988

return Term;

989

}

990

991

TERM eml_SimplifyQuantors(TERM Term)

992

/**************************************************************

993

INPUT: A formula.

994

RETURNS: The formula after

995

removal of bindings of variables that don't occur in the

996

respective subformula and possible mergings of quantors

997

CAUTION: The term is destrucively changed.

998

NOTE: This procedure conincides with cnf_SimplifyQuantors()

999

***************************************************************/

1000

{

1001

SYMBOL Top;

1002

LIST Scan;

1003

1004

Top = term_TopSymbol(Term);

1005

1006

if (symbol_IsPredicate(Top) || symbol_Equal(Top,fol_Varlist()))

1007

return Term;

1008

1009

if (fol_IsQuantifier(Top)) {

1010

LIST Vars;

1011

TERM Var,Subterm,Aux;

1012

Vars = list_Nil();

1013

Subterm = term_SecondArgument(Term);

1014

1015

while (symbol_Equal(term_TopSymbol(Subterm),Top)) {

1016

term_RplacArgumentList(term_FirstArgument(Term),

1017

list_Nconc(fol_QuantifierVariables(Term),fol_QuantifierVariables(Subterm)));

1018

term_Free(term_FirstArgument(Subterm));

1019

Aux = term_SecondArgument(Subterm);

1020

list_Delete(term_ArgumentList(Subterm));

1021

term_Free(Subterm);

1022

list_Rplaca(list_Cdr(term_ArgumentList(Term)),Aux);

1023

Subterm = Aux;

1024

}

1025

1026

for(Scan=fol_QuantifierVariables(Term);!list_Empty(Scan);Scan=list_Cdr(Scan)) {

1027

Var = (TERM)list_Car(Scan);

1028

if (!fol_VarOccursFreely(Var,Subterm))

1029

Vars = list_Cons(Var,Vars);

1030

}

1031

if (!list_Empty(Vars)) {

1032

Subterm = term_FirstArgument(Term);

1033

term_RplacArgumentList(Subterm,list_NPointerDifference(term_ArgumentList(Subterm),Vars));

1034

list_DeleteWithElement(Vars, (void (*)())term_Delete);

1035

if (list_Empty(term_ArgumentList(Subterm))) {

1036

Subterm = term_SecondArgument(Term);

1037

term_Delete(term_FirstArgument(Term));

1038

list_Delete(term_ArgumentList(Term));

1039

term_Free(Term);

1040

return eml_SimplifyQuantors(Subterm);

1041

}

1042

}

1043

}

1044

1045

for (Scan=term_ArgumentList(Term);!list_Empty(Scan);Scan=list_Cdr(Scan))

1046

list_Rplaca(Scan,eml_SimplifyQuantors(list_Car(Scan)));

1047

1048

return Term;

1049

}

1050

1051

TERM eml_ObviousSimplifications(TERM Term, FLAGSTORE Flags)

1052

/**************************************************************

1053

INPUT: An eml formula.

1054

RETURNS: The formula after performing the following simplifications:

1055

- eliminate true, false, id, etc

1056

- remove "or" and "and" with only one argument

1057

- merge quantors

1058

CAUTION: The term is destructively changed.

1059

NOTE: This does not obliviate simplification of the first-order

1060

formula. E.g. dia(alpha,true) cannot be reduced in the modal

1061

context.

1062

Nested expression of n-ary associative operations (and, comp,

1063

...) are reduced later.

1064

***************************************************************/

1065

{

1066

Term = eml_RemoveTrivialAtomsAndOps(Term);

1067

Term = eml_SimplifyQuantors(Term); /* strictly only needed for non-propositional formulae */

1068

1069

/* Attempt to eliminate composition by applying */

1070

if (flag_GetFlagIntValue(Flags, flag_EMLELIMCOMP)) {

1071

Term = eml_MakeOneAndOrCompSum(Term);

1072

Term = eml_EliminateComp(Term);

1073

}

1074

1075

return Term;

1076

}

1077

1078

BOOL eml_IsPropositional(TERM Term)

1079

/**************************************************************

1080

INPUT: A formula.

1081

RETURNS: True, if formula does not contain an n-ary predicate symbol

1082

or a first order quantifier.

1083

***************************************************************/

1084

{

1085

LIST Scan;

1086

BOOL result;

1087

1088

result = TRUE;

1089

if (term_IsComplex(Term)) {

1090

if (symbol_IsPredicate(term_TopSymbol(Term)) ||

1091

fol_IsQuantifier(term_TopSymbol(Term)))

1092

return FALSE;

1093

else

1094

for(Scan=term_ArgumentList(Term); result && !list_Empty(Scan); Scan=list_Cdr(Scan))

1095

result = eml_IsPropositional(list_Car(Scan));

1096

}

1097

1098

return result;

1099

}

1100

1101

static TERM eml_RplacPropByFoAtom(TERM Atom, eml_SYMBOLTYPE SymbolType,

1102

int Arity, LIST Args, FLAGSTORE Flags, PRECEDENCE Precedence)

1103

/**************************************************************

1104

INPUT: A propositional atom, a symbol type, a natural number, and a

1105

list of variables.

1106

RETURNS: A first-order atom with the specified arity formed with the

1107

symbol of the specified type and the specified arguments.

1108

The predicate name is built from the propositional name.

1109

EFFECT: If the predicate symbol does not exist in the signature it is

1110

created and inherits its precedence setting.

1111

CAUTION: The atom is destructively changed.

1112

***************************************************************/

1113

{

1114

SYMBOL propSymbol, foSymbol;

1115

1116

#ifdef DEBUG

1117

if (list_Empty(term_ArgumentList(Atom)) {

1118

misc_StartErrorReport();

1119

misc_ErrorReport("\n In eml_RplacPropByFoAtom: Propositional atom must not have argument list.");

1120

misc_FinishErrorReport();

1121

}

1122

#endif

1123

1124

propSymbol = term_TopSymbol(Atom);

1125

1126

if (symbol_Equal(propSymbol, fol_True()) ||

1127

symbol_Equal(propSymbol, fol_False())) {

1128

list_DeleteWithElement(Args, (void (*)())term_Delete);

1129

return Atom; /* Attempt to simplify ?? */

1130

}

1131

1132

if (symbol_Equal(propSymbol, eml_Id())) { /* Arguments should be nil, propositional */

1133

symbol_SetOrdering(Precedence, fol_Equality(), symbol_Ordering(Precedence, eml_Id()));

1134

return eml_RplacWithOpAndArgs(Atom, fol_Equality(), Args);

1135

}

1136

else if (symbol_Equal(propSymbol, eml_Div())) {

1137

return eml_RplacWithOpAndArgs(Atom, fol_Not(),

1138

list_List(term_Create(fol_Equality(), Args)));

1139

}

1140

1141

foSymbol = eml_GetFoSymbolAssocWithPropSymbol(propSymbol, Arity, SymbolType);

1142

1143

#ifdef DEBUG

1144

if (!eml_NaryType(SymbolType) && (foSymbol != symbol__NULL) &&

1145

(symbol_Arity(foSymbol) != Arity)) {

1146

fprintf(stderr, "Symbol %s declared with arity %d, but arity %d required\n",

1147

symbol_Name(foSymbol), symbol_Arity(foSymbol),Arity);

1148

misc_Error();

1149

return NULL;

1150

}

1151

#endif

1152

1153

if (foSymbol == symbol__NULL) {

1154

foSymbol = eml_CreateFoSymbol(propSymbol, SymbolType, Arity, symbol_STATLEX, Precedence);

1155

/* Precedence among the first-order symbols is inherited from that among

1156

* the propositional symbols */

1157

symbol_SetOrdering(Precedence, foSymbol,symbol_Ordering(Precedence, propSymbol));

1158

}

1159

1160

return eml_RplacWithOpAndArgs(Atom, foSymbol, Args);

1161

}

1162

1163

SYMBOL eml_CreateNarySymbol(SYMBOL PropSymbol, eml_SYMBOLTYPE SymbolType,

1164

const char* NameSuffix, int Arity, int Status, PRECEDENCE Precedence)

1165

/*******************************************************

1166

INPUT: A symbol (which MUST be a propositonal symbol/nullary

1167

predicate symbol), a symbol type (of the fo symbol to be

1168

created), the predefined name suffix, the arity of the new

1169

symbol, the status of the new symbol.

1170

RETURNS: A first-order symbol corresponding to PropSymbol (special for

1171

the functial translation in terms of n-ary predicates with the sorts

1172

encoded in the predicate names).

1173

REMARK: Similar to dfg_SymbolDecl. Prototypical.

1174

********************************************************/

1175

{

1176

int size;

1177

char* newName;

1178

char* arityStr;

1179

SYMBOL symbol;

1180

1181

arityStr = string_IntToString(Arity);

1182

1183

size = strlen(eml_PREDNAMEPREFIX[SymbolType])+strlen(symbol_Name(PropSymbol))+1+strlen(arityStr)+strlen(NameSuffix)+1;

1184

newName = (char*)memory_Malloc(sizeof(char)*size);

1185

sprintf(newName,"%s%s_%s%s", eml_PREDNAMEPREFIX[SymbolType],symbol_Name(PropSymbol), arityStr, NameSuffix);

1186

1187

/* Check if this symbol was declared earlier */

1188

symbol = symbol_Lookup(newName);

1189

if (symbol != 0) {

1190

/* Symbol was declared before

1191

* Check if the old and new symbol type are equal */

1192

/* Eventually we would want more checking to be done here, i.e.

1193

* we need new designated symbol types */

1194

if ( !symbol_IsPredicate(symbol)) {

1195

fprintf(stderr, "In eml_CreateNarySymbol: Symbol %s was already declared as ",

1196

newName);

1197

switch (symbol_Type(symbol)) {

1198

case symbol_CONSTANT:

1199

case symbol_FUNCTION:

1200

fputs("function\n", stderr); break;

1201

case symbol_JUNCTOR:

1202

fputs("junctor", stderr); break;

1203

default:

1204

fputs("unknown non-predicate type\n", stderr);

1205

}

1206

misc_Error();

1207

}

1208

/* Now check the old and new arity if specified */

1209

if (Arity != -2 && Arity != symbol_Arity(symbol)) {

1210

fprintf(stderr, "In eml_CreateNarySymbol: Symbol %s was already declared with arity %d\n",

1211

newName, symbol_Arity(symbol));

1212

misc_Error();

1213

}

1214

} else

1215

/* Symbol was not declared before */

1216

symbol = symbol_CreatePredicate(newName, Arity, Status, Precedence);

1217

1218

string_StringFree(arityStr);

1219

memory_Free(newName,sizeof(char)*size);

1220

1221

return symbol;

1222

}

1223

1224

static TERM eml_RplacPropByNaryAtom(TERM Atom, eml_SYMBOLTYPE

1225

SymbolType, char* NameSuffix, int Arity, LIST Args,

1226

FLAGSTORE Flags, PRECEDENCE Precedence)

1227

/**************************************************************

1228

INPUT: A propositional atom, a symbol type, a string, a natural

1229

number, and a list of variables.

1230

RETURNS: A first-order atom with the specified arity formed with the

1231

symbol of the specified type and the specified arguments.

1232

The predicate name is built from the propositional name and

1233

(different from eml_RplacPropByFoAtom) the given name suffix.

1234

EFFECT: A new predicate symbol is created and inherits its precedence

1235

setting.

1236

CAUTION: The atom is destructively changed.

1237

***************************************************************/

1238

{

1239

SYMBOL propSymbol, foSymbol;

1240

1241

propSymbol = term_TopSymbol(Atom);

1242

1243

if (symbol_Equal(propSymbol,fol_True()) || symbol_Equal(propSymbol,fol_False())) {

1244

list_DeleteWithElement(Args, (void (*)())term_Delete);

1245

return Atom;

1246

}

1247

1248

if (flag_GetFlagIntValue(Flags, flag_EMLFFSORTS)) /* with explicit sorts */

1249

foSymbol = eml_CreateNarySymbol(propSymbol, SymbolType,

1250

symbol_Name(propSymbol), Arity, symbol_STATLEX, Precedence);

1251

else /* sort info encoded in predicate names */

1252

foSymbol = eml_CreateNarySymbol(propSymbol, SymbolType, NameSuffix, Arity,

1253

symbol_STATLEX, Precedence);

1254

symbol_SetOrdering(Precedence, foSymbol,symbol_Ordering(Precedence, propSymbol)); /* ?? */

1255

1256

return eml_RplacWithOpAndArgs(Atom, foSymbol, Args);

1257

}

1258

1259

static TERM eml_EmbedInRelCalculusProp(TERM Term)

1260

/**************************************************************

1261

INPUT: An Eml (propositional) formula.

1262

RETURNS: Its translation into a relational formula as a right

1263

injective formula.

1264

CAUTION: The term is destructively changed.

1265

***************************************************************/

1266

{

1267

SYMBOL Top;

1268

1269

Top = term_TopSymbol(Term);

1270

1271

/* Term = p */

1272

if (symbol_IsPredicate(Top)) {

1273

list_Delete(term_ArgumentList(Term)); /* shouldn't be needed */

1274

return eml_RplacWithOpAndArgs(Term, eml_Comp(),

1275

list_Cons(term_Copy(Term),

1276

list_List(term_Create(fol_True(), list_Nil()))));

1277

/* comp(p,true) */

1278

}

1279

/* Term = not(phi), or(...), and(...), comp(...), sum(...),

1280

* test(phi), domrestr(...), ranrestr(...) */

1281

else if (eml_IsRelationalJunctor(Top)) { /* Seems strange, but makes sense */

1282

LIST Scan;

1283

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))

1284

eml_EmbedInRelCalculusProp(list_Car(Scan));

1285

return Term;

1286

}

1287

/* Term = dia(alpha,phi) */

1288

else if (symbol_Equal(Top, eml_Dia())) {

1289

LIST args;

1290

args = list_Cons(eml_EmbedInRelCalculusRel(term_FirstArgument(Term)),

1291

list_List(eml_EmbedInRelCalculusProp(term_SecondArgument(Term))));

1292

list_Delete(term_ArgumentList(Term));

1293

return eml_RplacWithOpAndArgs(Term, eml_Comp(), args);

1294

/* comp(alpha,tr(phi)) */

1295

}

1296

/* Term = box(alpha,phi) */

1297

else if (symbol_Equal(Top, eml_Box())) {

1298

TERM helpTerm;

1299

helpTerm = term_Create(eml_Comp(),

1300

list_Cons(eml_EmbedInRelCalculusRel(term_FirstArgument(Term)),

1301

list_List(term_Create(fol_Not(),

1302

list_List(eml_EmbedInRelCalculusProp(term_SecondArgument(Term)))))));

1303

list_Delete(term_ArgumentList(Term));

1304

return eml_RplacWithOpAndArgs(Term, fol_Not(), list_List(helpTerm));

1305

/* not(comp(alpha,not(tr(phi)))) */

1306

}

1307

/* Term = domain(alpha) or Term = range(alpha) */

1308

else if (symbol_Equal(Top,eml_Domain()) || symbol_Equal(Top,eml_Range())) {

1309

LIST args;

1310

term_RplacTop(Term, eml_Comp());

1311

if (symbol_Equal(Top,eml_Domain()))

1312

args = list_Cons(eml_EmbedInRelCalculusRel(term_FirstArgument(Term)),

1313

list_List(term_Create(fol_True(), list_Nil())));

1314

else

1315

args = list_Cons(term_Create(fol_True(), list_Nil()),

1316

list_List(eml_EmbedInRelCalculusRel(term_FirstArgument(Term))));

1317

list_Delete(term_ArgumentList(Term));

1318

term_RplacArgumentList(Term,args);

1319

1320

return Term;

1321

/* comp(alpha,true) or comp(true,alpha) */

1322

}

1323

else {

1324

fprintf(stderr, "\nNo case for %s in eml_EmbedInRelCalculusProp()\n",

1325

symbol_Name(Top));

1326

misc_Error();

1327

return NULL;

1328

}

1329

1330

}

1331

1332

static TERM eml_EmbedInRelCalculusRel(TERM Term)

1333

/**************************************************************

1334

INPUT: An Eml (propositional) formula.

1335

RETURNS: Its translation into a relational formula as a right

1336

injective formula.

1337

CAUTION: The term is destructively changed.

1338

***************************************************************/

1339

{

1340

SYMBOL Top;

1341

LIST args;

1342

1343

Top = term_TopSymbol(Term);

1344

1345

/* Term = p */

1346

if (symbol_IsPredicate(Top)) {

1347

return Term;

1348

}

1349

/* Term = test(phi) */

1350

else if (symbol_Equal(Top, eml_Test())) {

1351

args = list_Cons(eml_EmbedInRelCalculusProp(term_FirstArgument(Term)),

1352

list_List(term_Create(eml_Id(), list_Nil())));

1353

list_Delete(term_ArgumentList(Term));

1354

return eml_RplacWithOpAndArgs(Term, fol_And(), args);

1355

/* tr(phi) /\ id */

1356

}

1357

/* Term = domrestr(alpha,phi) */

1358

else if (symbol_Equal(Top, eml_DomRestr())) {

1359

args = list_Cons(term_FirstArgument(Term),

1360

list_List(eml_EmbedInRelCalculusProp(term_SecondArgument(Term))));

1361

list_Delete(term_ArgumentList(Term));

1362

return eml_RplacWithOpAndArgs(Term, fol_And(), args);

1363

/* alpha /\ tr(phi) */

1364

}

1365

/* Term = ranrestr(alpha,phi) */

1366

else if (symbol_Equal(Top, eml_RanRestr())) {

1367

args = list_Cons(term_FirstArgument(Term),

1368

list_List(term_Create(eml_Conv(),

1369

list_List(eml_EmbedInRelCalculusProp(term_SecondArgument(Term))))));

1370

list_Delete(term_ArgumentList(Term));

1371

return eml_RplacWithOpAndArgs(Term, fol_And(), args);

1372

/* alpha /\ conv(tr(phi)) */

1373

}

1374

/* Term = not(phi), or(...), and(...), comp(...), sum(...) */

1375

/* It is important that this test is done last */

1376

else if (eml_IsRelationalJunctor(Top)) {

1377

LIST Scan;

1378

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))

1379

eml_EmbedInRelCalculusRel(list_Car(Scan));

1380

return Term;

1381

}

1382

else {

1383

fprintf(stderr, "\nNo case for %s in eml_EmbedInRelCalculusRel()\n",

1384

symbol_Name(Top));

1385

misc_Error();

1386

return NULL;

1387

}

1388

1389

}

1390

1391

1392

static TERM eml_RelationalTranslationProp(TERM Term, SYMBOL Var,

1393

FLAGSTORE Flags, PRECEDENCE Precedence)

1394

/**************************************************************

1395

INPUT: An eml (propositional) formula and a variable (the free variable).

1396

RETURNS: Its standard (relational) translation.

1397

CAUTION: The term is destructively changed.

1398

***************************************************************/

1399

{

1400

SYMBOL Top;

1401

1402

Top = term_TopSymbol(Term);

1403

1404

/* Term = p */

1405

if (symbol_IsPredicate(Top)) {

1406

return eml_RplacPropByFoAtom(Term, eml_PROP, 1, list_List(term_Create(Var,list_Nil())), Flags, Precedence);

1407

}

1408

/* Term = not(phi), Term = or(...) or Term = and(...) */

1409

else if (eml_IsPropJunctor(Top)) {

1410

LIST Scan;

1411

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))

1412

eml_RelationalTranslationProp(list_Car(Scan),Var, Flags, Precedence);

1413

return Term;

1414

}

1415

/* Term = dia(alpha,phi) or Term = box(alpha,phi) */

1416

else if (eml_IsModalOpSymbol(Top)) {

1417

SYMBOL newVar;

1418

TERM helpTerm;

1419

newVar = symbol_CreateStandardVariable();

1420

helpTerm = term_Create(eml_FoJunctorAssocWithPropSymbol(Top),

1421

list_Cons(eml_RelationalTranslationRel(term_FirstArgument(Term),Var,newVar, Flags, Precedence),

1422

list_List(eml_RelationalTranslationProp(term_SecondArgument(Term),newVar, Flags, Precedence))));

1423

list_Delete(term_ArgumentList(Term));

1424

return eml_RplacWithQuantifier(Term, eml_FoQuantAssocWithPropSymbol(Top), list_List(term_Create(newVar,list_Nil())),

1425

list_List(helpTerm));

1426

/* exists y tr(alpha)(x,y) /\ tr(phi)(y) or

1427

* forall y tr(alpha)(x,y) -> tr(phi)(y) */

1428

}

1429

/* Term = domain(alpha) or Term = range(alpha) */

1430

else if (symbol_Equal(Top,eml_Domain()) || symbol_Equal(Top,eml_Range())) {

1431

SYMBOL newVar;

1432

TERM helpTerm;

1433

newVar = symbol_CreateStandardVariable();

1434

if (symbol_Equal(Top,eml_Domain()))

1435

helpTerm = eml_RelationalTranslationRel(term_FirstArgument(Term),Var,newVar, Flags, Precedence);

1436

else

1437

helpTerm = eml_RelationalTranslationRel(term_FirstArgument(Term),newVar,Var, Flags, Precedence);

1438

1439

list_Delete(term_ArgumentList(Term));

1440

return eml_RplacWithQuantifier(Term, eml_FoQuantAssocWithPropSymbol(Top), list_List(term_Create(newVar,list_Nil())),

1441

list_List(helpTerm));

1442

/* exists y tr(alpha)(x,y) or exists y tr(alpha)(y,x) */

1443

}

1444

else {

1445

fprintf(stderr, "\nNo case for %s in eml_RelationalTranslationProp()\n",

1446

symbol_Name(Top));

1447

misc_Error();

1448

return NULL;

1449

}

1450

1451

}

1452

1453

static TERM eml_RelationalTranslationRel(TERM Term, SYMBOL VarX, SYMBOL VarY,

1454

FLAGSTORE Flags, PRECEDENCE Precedence)

1455

/**************************************************************

1456

INPUT: An eml (relational) formula, two variables (the free

1457

variables), a string encoding of the sorts of the arguments

1458

and the modal depth.

1459

RETURNS: Its standard (relational) translation.

1460

CAUTION: The term is destructively changed.

1461

***************************************************************/

1462

{

1463

SYMBOL Top;

1464

1465

Top = term_TopSymbol(Term);

1466

1467

/* Term = r */

1468

if (symbol_IsPredicate(Top)) {

1469

return eml_RplacPropByFoAtom(Term, eml_REL, 2, list_Cons(term_Create(VarX,list_Nil()),list_List(term_Create(VarY,list_Nil()))), Flags, Precedence);

1470

}

1471

/* Term = not(alpha), Term = or(...) or Term = and(...) */

1472

else if (eml_IsPropJunctor(Top)) {

1473

LIST Scan;

1474

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))

1475

eml_RelationalTranslationRel(list_Car(Scan),VarX,VarY, Flags, Precedence);

1476

return Term;

1477

}

1478

/* Term = conv(alpha) */

1479

else if (symbol_Equal(Top,eml_Conv())) {

1480

TERM helpTerm;

1481

helpTerm = eml_RelationalTranslationRel(term_FirstArgument(Term),VarY,VarX, Flags, Precedence);

1482

list_Delete(term_ArgumentList(Term));

1483

Term = eml_RplacWithOpAndArgs(Term, term_TopSymbol(helpTerm),

1484

term_ArgumentList(helpTerm));

1485

term_Free(helpTerm);

1486

return Term;

1487

/* tr(alpha)(y,x) */

1488

}

1489

/* Term = comp(...) or sum(...)*/

1490

else if (symbol_Equal(Top,eml_Comp()) || symbol_Equal(Top,eml_Sum())) {

1491

SYMBOL var, newVar;

1492

TERM helpTerm;

1493

LIST Scan, varList;

1494

var = VarX;

1495

varList = list_Nil();

1496

for (Scan=term_ArgumentList(Term); !list_Empty(list_Cdr(Scan)); Scan=list_Cdr(Scan)) {

1497

newVar = symbol_CreateStandardVariable();

1498

varList = list_Nconc(varList, list_List(term_Create(newVar,list_Nil())));

1499

eml_RelationalTranslationRel(list_Car(Scan),var,newVar, Flags, Precedence);

1500

var = newVar;

1501

}

1502

eml_RelationalTranslationRel(list_Car(Scan),var,VarY, Flags, Precedence);

1503

1504

helpTerm = term_Create(eml_FoJunctorAssocWithPropSymbol(Top), term_ArgumentList(Term)); /* Sharing including argument list */

1505

return eml_RplacWithQuantifier(Term,

1506

eml_FoQuantAssocWithPropSymbol(Top), varList, list_List(helpTerm));

1507

/* exists z1,z2 tr(alpha1)(x,z1) /\ tr(alpha2)(z1,z2) /\ tr(alpha3)(z2,y) ... or

1508

* forall z1,z2 tr(alpha1)(x,z1) \/ tr(alpha2)(z1,z2) \/ tr(alpha3)(z2,y) ... */

1509

}

1510

/* Term = test(phi) */

1511

else if (symbol_Equal(Top,eml_Test())) {

1512

TERM helpTerm;

1513

helpTerm = eml_RelationalTranslationProp(term_FirstArgument(Term),VarY, Flags, Precedence);

1514

list_Delete(term_ArgumentList(Term));

1515

return eml_RplacWithOpAndArgs(Term, fol_And(),

1516

list_Cons(term_Create(fol_Equality(),

1517

list_Cons(term_Create(VarX,list_Nil()), list_List(term_Create(VarY,list_Nil())))),

1518

list_List(helpTerm)));

1519

/* equal(x,y) /\ tr(phi)(y) */

1520

}

1521

/* Term = domrestr(alpha,phi) or ranrestr(alpha,phi) */

1522

else if (symbol_Equal(Top,eml_DomRestr()) || symbol_Equal(Top,eml_RanRestr())) {

1523

TERM helpTerm, helpTermRel;

1524

helpTermRel = eml_RelationalTranslationRel(term_FirstArgument(Term),VarX,VarY, Flags, Precedence);

1525

if (symbol_Equal(Top,eml_DomRestr()))

1526

helpTerm = eml_RelationalTranslationProp(term_SecondArgument(Term),VarX, Flags, Precedence);

1527

else

1528

helpTerm = eml_RelationalTranslationProp(term_SecondArgument(Term),VarY, Flags, Precedence);

1529

list_Delete(term_ArgumentList(Term));

1530

return eml_RplacWithOpAndArgs(Term, fol_And(),

1531

list_Cons(helpTermRel, list_List(helpTerm)));

1532

/* tr(alpha)(x,y) /\ tr(phi)(x) or tr(alpha)(x,y) /\ tr(phi)(y) */

1533

}

1534

else {

1535

fprintf(stderr, "\nNo case for %s in eml_RelationalTranslationRel()\n",

1536

symbol_Name(Top));

1537

misc_Error();

1538

return NULL;

1539

}

1540

1541

}

1542

1543

static TERM eml_RelationalTranslation(TERM Term, FLAGSTORE Flags, PRECEDENCE Precedence)

1544

/**************************************************************

1545

INPUT: An eml (propositional) formula.

1546

RETURNS: Its standard (relational) translation.

1547

CAUTION: The term is destructively changed.

1548

***************************************************************/

1549

{

1550

TERM newVarX, helpTerm;

1551

1552

symbol_ResetStandardVarCounter();

1553

1554

newVarX = term_Create(symbol_CreateStandardVariable(), list_Nil());

1555

1556

/* Embedding into the relational calculus */

1557

if (flag_GetFlagIntValue(Flags, flag_EML2REL)) {

1558

TERM newVarY;

1559

1560

Term = eml_EmbedInRelCalculusProp(Term);

1561

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

1562

printf("\n [Rel] \t");fol_PrintDFG(Term);

1563

}

1564

1565

newVarY = term_Create(symbol_CreateStandardVariable(), list_Nil());

1566

helpTerm = eml_RelationalTranslationRel(Term,term_TopSymbol(newVarX),term_TopSymbol(newVarY), Flags, Precedence);

1567

1568

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

1569

printf("\n [RelTr] \t");

1570

return term_Create(fol_All(), list_Cons(term_Create(fol_Varlist(),list_Cons(newVarX,list_List(newVarY))), list_List(helpTerm)));

1571

/* forall x y tr(Term,x,y) */

1572

}

1573

/* Relational functional/path-based translation */

1574

else if (flag_GetFlagIntValue(Flags, flag_EMLFNARY)) {

1575

char nameSuffix[] = "";

1576

1577

flag_SetFlagIntValue(Flags, flag_EMLFFSORTS, flag_EMLFFSORTSOFF);

1578

/* Don't use explicit sorts! Important for creation of

1579

* new atoms in eml_RplacPropByNaryAtom() */

1580

1581

helpTerm = eml_RelFunctTranslProp(Term, term_TopSymbol(newVarX), nameSuffix, Flags, Precedence);

1582

1583

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

1584

printf("\n [RelFuncTr] \t");

1585

return term_Create(fol_All(), list_Cons(term_Create(fol_Varlist(),list_List(newVarX)), list_List(helpTerm)));

1586

}

1587

/* Standard relational translation */

1588

else {

1589

helpTerm = eml_RelationalTranslationProp(Term,term_TopSymbol(newVarX), Flags, Precedence);

1590

1591

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

1592

printf("\n [RelTr] \t");

1593

return term_Create(fol_All(), list_Cons(term_Create(fol_Varlist(),list_List(newVarX)), list_List(helpTerm)));

1594

/* forall x tr(Term,x) */

1595

}

1596

}

1597

1598

static TERM eml_FunctTranslItoNaryPredProp(TERM Term, LIST VarList,

1599

char* SortEncoding, int VarListLength,

1600

FLAGSTORE Flags, PRECEDENCE Precedence)

1601

/**************************************************************

1602

INPUT: An eml (propositional) formula, a variable list, a string

1603

encoding of the sorts of the arguments and the length of the

1604

list of variables.

1605

RETURNS: Its functional translation ito n-ary predicates.

1606

CAUTION: The term is destructively changed.

1607

***************************************************************/

1608

{

1609

SYMBOL Top;

1610

1611

Top = term_TopSymbol(Term);

1612

1613

#ifdef DEBUG

1614

if (VarListLength != list_Length(VarList)) {

1615

fprintf(stderr, "Arity VarListLength conflict\n");

1616

misc_Error();

1617

return NULL;

1618

}

1619

#endif

1620

1621

/* Term = p */

1622

if (symbol_IsPredicate(Top)) {

1623

VarList = list_CopyWithElement(VarList,(POINTER (*)())term_Copy);

1624

return eml_RplacPropByNaryAtom(Term, eml_NARYPROP, SortEncoding,

1625

VarListLength, VarList, Flags, Precedence);

1626

}

1627

/* Term = not(phi), Term = or(...) or Term = and(...) */

1628

else if (eml_IsPropJunctor(Top)) {

1629

LIST Scan;

1630

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))

1631

eml_FunctTranslItoNaryPredProp(list_Car(Scan), VarList,

1632

SortEncoding, VarListLength, Flags, Precedence);

1633

return Term;

1634

}

1635

/* Term = dia(r,phi) or Term = box(r,phi) */

1636

else if (eml_IsModalOpSymbol(Top)) {

1637

TERM relSubTerm, newVar, helpTerm, anotherHelpTerm;

1638

LIST newVarList;

1639

char* newSortEncoding;

1640

int size;

1641

1642

relSubTerm = term_FirstArgument(Term);

1643

newVar = term_Create(symbol_CreateStandardVariable(), list_Nil());

1644

newVarList = list_Nconc(list_CopyWithElement(VarList,(POINTER (*)())term_Copy), list_List(newVar));

1645

1646

size = strlen(SortEncoding)+strlen(symbol_Name(term_TopSymbol(relSubTerm)))+1;

1647

newSortEncoding = memory_Malloc(size*sizeof(char));

1648

sprintf(newSortEncoding,"%s%s", SortEncoding, symbol_Name(term_TopSymbol(relSubTerm)));

1649

1650

if (flag_GetFlagIntValue(Flags, flag_EMLFUNCNDEQ)) {

1651

helpTerm = eml_BuildSortQuantifierFor(Term, Top, term_TopSymbol(relSubTerm),

1652

term_TopSymbol(newVar), flag_GetFlagIntValue(Flags, flag_EMLFFSORTS),

1653

list_List(eml_FunctTranslItoNaryPredProp(term_SecondArgument(Term),

1654

newVarList, newSortEncoding, VarListLength+1, Flags, Precedence)),

1655

(POINTER (*)())eml_CreateQuantifier, Precedence);

1656

list_Delete(term_ArgumentList(Term));

1657

anotherHelpTerm = eml_RplacWithOpAndArgs(Term, eml_FoJunctorAssocWithPropSymbol(Top),

1658

list_Cons(eml_FunctTranslItoNaryPredRel(relSubTerm,

1659

VarList, SortEncoding, VarListLength, Flags, Precedence),

1660

list_List(helpTerm)));

1661

list_DeleteWithElement(newVarList,(void (*)())term_Delete);

1662

return anotherHelpTerm;

1663

/* nde_r(vl) /\ exists y_r tr(phi)(vl,y) or

1664

* nde_r(vl) -> forall y_r tr(phi)(vl,y) */

1665

}

1666

else {

1667

TERM relSubTermCopy = term_Copy(relSubTerm); /* make a copy; important */

1668

helpTerm = term_Create(eml_FoJunctorAssocWithPropSymbol(Top),

1669

list_Cons(eml_FunctTranslItoNaryPredRel(relSubTerm,

1670

VarList, SortEncoding, VarListLength, Flags, Precedence),

1671

list_List(eml_FunctTranslItoNaryPredProp(term_SecondArgument(Term),

1672

newVarList, newSortEncoding, VarListLength+1, Flags, Precedence))));

1673

list_Delete(term_ArgumentList(Term));

1674

anotherHelpTerm = eml_BuildSortQuantifierFor(Term, Top,

1675

term_TopSymbol(relSubTermCopy), term_TopSymbol(newVar),

1676

flag_GetFlagIntValue(Flags, flag_EMLFFSORTS),

1677

list_List(helpTerm), (POINTER (*)())eml_RplacWithQuantifier, Precedence);

1678

list_DeleteWithElement(newVarList,(void (*)())term_Delete);

1679

term_Delete(relSubTermCopy);

1680

return anotherHelpTerm;

1681

/* exists y_r nde_r(vl) /\ tr(phi)(vl,y) or

1682

* forall y_r nde_r(vl) -> tr(phi)(vl,y) */

1683

}

1684

1685

memory_Free(newSortEncoding,size*sizeof(char));

1686

}

1687

else {

1688

fprintf(stderr, "\nNo case for %s in eml_FunctTranslItoNaryPredProp()\n",

1689

symbol_Name(Top));

1690

misc_Error();

1691

return NULL;

1692

}

1693

1694

}

1695

1696

static TERM eml_FunctTranslItoNaryPredRel(TERM Term, LIST VarList,

1697

char* SortEncoding, int VarListLength,

1698

FLAGSTORE Flags, PRECEDENCE Precedence)

1699

/**************************************************************

1700

INPUT: An EML relational formula, a variable list, a string (encoding

1701

the sorts of the accessibility relations in the scope), and

1702

the length of the variable list (corresponds to the modal

1703

depth).

1704

RETURNS: Its functional translation ito n-ary predicates.

1705

CAUTION: The term is destructively changed.

1706

***************************************************************/

1707

{

1708

SYMBOL Top;

1709

1710

Top = term_TopSymbol(Term);

1711

1712

/* Term = r */

1713

if (symbol_IsPredicate(Top)) {

1714

switch (flag_GetFlagIntValue(Flags, flag_EMLTHEORY)) {

1715

case flag_EMLTHEORYKD:

1716

return eml_RplacWithDesignatedPropAtom(Term, fol_True());

1717

break;

1718

case flag_EMLTHEORYK:

1719

VarList = list_CopyWithElement(VarList,(POINTER (*)())term_Copy);

1720

return eml_RplacPropByNaryAtom(Term, eml_NARYNDE,

1721

SortEncoding, VarListLength, VarList, Flags, Precedence);

1722

break;

1723

default:

1724

fprintf(stderr, "\nThe option EMLTheory = %d is not implemented in eml_FunctTranslItoNaryPredRel()\n",

1725

flag_GetFlagIntValue(Flags, flag_EMLTHEORY));

1726

misc_Error();

1727

return NULL;

1728

break;

1729

}

1730

}

1731

else {

1732

fprintf(stderr, "\nNo case for %s in eml_FunctTranslItoNaryPredRel()\n",

1733

symbol_Name(Top));

1734

misc_Error();

1735

return NULL;

1736

}

1737

}

1738

1739

static TERM eml_FunctTranslProp(TERM Term, TERM WorldPath,

1740

FLAGSTORE Flags, PRECEDENCE Precedence)

1741

/**************************************************************

1742

INPUT: An eml (propositional) formula, a variable list and its

1743

length.

1744

RETURNS: Its functional translation.

1745

CAUTION: The term is destructively changed.

1746

NOTE: WorldPath needs to be copied before it is "used"

1747

***************************************************************/

1748

{

1749

SYMBOL Top;

1750

1751

Top = term_TopSymbol(Term);

1752

1753

/* Term = p */

1754

if (symbol_IsPredicate(Top)) {

1755

return eml_RplacPropByFoAtom(Term, eml_PROP, 1, list_List(term_Copy(WorldPath)), Flags, Precedence);

1756

}

1757

/* Term = not(phi), Term = or(...) or Term = and(...) */

1758

else if (eml_IsPropJunctor(Top)) {

1759

LIST Scan;

1760

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))

1761

eml_FunctTranslProp(list_Car(Scan), WorldPath, Flags, Precedence);

1762

return Term;

1763

}

1764

/* Term = dia(alpha,phi) or Term = box(alpha,phi) */

1765

else if (eml_IsModalOpSymbol(Top)) {

1766

TERM newVar, newWorldPath, relSubTerm, helpTerm, anotherHelpTerm;

1767

relSubTerm = term_FirstArgument(Term);

1768

newVar = term_Create(symbol_CreateStandardVariable(), list_Nil());

1769

newWorldPath = term_Create(eml_ApplyFunct(), list_Cons(term_Copy(WorldPath),

1770

list_List(newVar)));

1771

if (flag_GetFlagIntValue(Flags, flag_EMLFUNCNDEQ)) {

1772

helpTerm = eml_BuildSortQuantifierFor(Term, Top, term_TopSymbol(relSubTerm),

1773

term_TopSymbol(newVar), TRUE,

1774

list_List(eml_FunctTranslProp(term_SecondArgument(Term),

1775

newWorldPath, Flags, Precedence)), (POINTER (*)())eml_CreateQuantifier, Precedence);

1776

/*printf("\n [*]\t"); fol_PrintDFG(helpTerm);*/

1777

list_Delete(term_ArgumentList(Term));

1778

anotherHelpTerm = eml_RplacWithOpAndArgs(Term, eml_FoJunctorAssocWithPropSymbol(Top),

1779

list_Cons(eml_FunctTranslRel(relSubTerm, WorldPath, Flags, Precedence),

1780

list_List(helpTerm)));

1781

/*printf("\n [**]\t"); fol_PrintDFG(anotherHelpTerm);*/

1782

term_Delete(newWorldPath);

1783

return anotherHelpTerm;

1784

/* nde_r(wp) /\ exists y_r tr(phi)(app(wp,y_r)) or

1785

* nde_r(wp) -> forall y_r tr(phi)(app(wp,y_r)) */

1786

}

1787

else {

1788

helpTerm = term_Create(eml_FoJunctorAssocWithPropSymbol(Top),

1789

list_Cons(eml_FunctTranslRel(relSubTerm, WorldPath, Flags, Precedence),

1790

list_List(eml_FunctTranslProp(term_SecondArgument(Term), newWorldPath, Flags, Precedence))));

1791

list_Delete(term_ArgumentList(Term));

1792

anotherHelpTerm = eml_BuildSortQuantifierFor(Term, Top, term_TopSymbol(relSubTerm),

1793

term_TopSymbol(newVar), TRUE,

1794

list_List(helpTerm), (POINTER (*)())eml_RplacWithQuantifier, Precedence);

1795

term_Delete(newWorldPath);

1796

return anotherHelpTerm;

1797

/* exists y_r nde_r(wp) /\ tr(phi)(app(wp,y_r)) or

1798

* forall y_r nde_r(wp) -> tr(phi)(app(wp,y_r)) */

1799

}

1800

}

1801

else {

1802

fprintf(stderr, "\nNo case for %s in eml_FunctTranslProp()\n",

1803

symbol_Name(Top));

1804

misc_Error();

1805

return NULL;

1806

}

1807

1808

}

1809

1810

static TERM eml_FunctTranslRel(TERM Term, TERM WorldPath,

1811

FLAGSTORE Flags, PRECEDENCE Precedence)

1812

/**************************************************************

1813

INPUT: An eml (propositional) formula, a variable list and its

1814

length.

1815

RETURNS: Its functional translation.

1816

CAUTION: The term is destructively changed.

1817

***************************************************************/

1818

{

1819

SYMBOL Top;

1820

1821

Top = term_TopSymbol(Term);

1822

1823

/* Term = r */

1824

if (symbol_IsPredicate(Top)) {

1825

switch (flag_GetFlagIntValue(Flags, flag_EMLTHEORY)) {

1826

case flag_EMLTHEORYKD:

1827

return eml_RplacWithDesignatedPropAtom(Term, fol_True());

1828

break;

1829

case flag_EMLTHEORYK:

1830

return eml_RplacPropByFoAtom(Term, eml_NDE, 1, list_List(term_Copy(WorldPath)), Flags, Precedence);

1831

break;

1832

default:

1833

fprintf(stderr, "\nThe option EMLTheory = %d is not implemented in eml_FunctTranslRel()\n",

1834

flag_GetFlagIntValue(Flags, flag_EMLTHEORY));

1835

misc_Error();

1836

return NULL;

1837

break;

1838

}

1839

}

1840

else {

1841

fprintf(stderr, "\nNo case for %s in eml_FunctTranslRel()\n",

1842

symbol_Name(Top));

1843

misc_Error();

1844

return NULL;

1845

}

1846

}

1847

1848

1849

static TERM eml_FunctionalTranslation(TERM Term, BOOL ItoNaryPreds,

1850

FLAGSTORE Flags, PRECEDENCE Precedence)

1851

/**************************************************************

1852

INPUT: An eml (propositional) formula and a flag.

1853

RETURNS: Its functional translation. If the flag is true the

1854

translation is into ordered first-order logic or the

1855

Bernays-Schoenfinkel class, meaning n-ary predicates

1856

are generated.

1857

CAUTION: The term is destructively changed.

1858

***************************************************************/

1859

{

1860

symbol_ResetStandardVarCounter();

1861

1862

if (ItoNaryPreds) {

1863

char nameSuffix[] = "";

1864

1865

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

1866

printf("\n [FuncFTr] \t");

1867

Term = eml_FunctTranslItoNaryPredProp(Term, list_Nil(), nameSuffix, 0, Flags, Precedence);

1868

/* Check whether sharing is possible on the name suffixes,

1869

* e.g. whether the iterative allocation of new memory in

1870

* eml_FunctTranslItoNaryPredProp is necessary. */

1871

return Term;

1872

/* note: without world quantifier */

1873

}

1874

else {

1875

TERM newVar, helpTerm;

1876

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

1877

printf("\n [FuncTr] \t");

1878

newVar = term_Create(symbol_CreateStandardVariable(), list_Nil());

1879

helpTerm = eml_FunctTranslProp(Term,newVar, Flags, Precedence);

1880

/*printf("\n [**]\t"); fol_PrintDFG(helpTerm);*/

1881

return term_Create(fol_All(), list_Cons(term_Create(fol_Varlist(),list_List(newVar)), list_List(helpTerm)));

1882

/* forall x tr(Term,x) */

1883

}

1884

1885

}

1886

1887

static TERM eml_SemiFunctTranslProp(TERM Term, TERM WorldTerm, int Polarity,

1888

FLAGSTORE Flags, PRECEDENCE Precedence)

1889

/**************************************************************

1890

INPUT: An eml (propositional) formula, term of type world, and the

1891

polarity of the formula (Term) in the original formula

1892

length.

1893

RETURNS: Its functional translation.

1894

CAUTION: The term is destructively changed.

1895

***************************************************************/

1896

{

1897

SYMBOL Top;

1898

1899

Top = term_TopSymbol(Term);

1900

1901

/* Term = p */

1902

if (symbol_IsPredicate(Top)) {

1903

return eml_RplacPropByFoAtom(Term, eml_PROP, 1, list_List(term_Copy(WorldTerm)), Flags, Precedence);

1904

}

1905

/* Term = not(phi) */

1906

else if (eml_IsNotSymbol(Top)) {

1907

eml_SemiFunctTranslProp(term_FirstArgument(Term),

1908

WorldTerm, Polarity * -1, Flags, Precedence);

1909

return Term;

1910

}

1911

/* Term = implies(...) */

1912

else if (eml_IsImpliesSymbol(Top)) {

1913

eml_SemiFunctTranslProp(term_FirstArgument(Term), WorldTerm, Polarity * -1, Flags, Precedence);

1914

eml_SemiFunctTranslProp(term_SecondArgument(Term), WorldTerm, Polarity, Flags, Precedence);

1915

return Term;

1916

}

1917

/* Term = implied(...) */

1918

else if (eml_IsImpliedSymbol(Top)) {

1919

eml_SemiFunctTranslProp(term_SecondArgument(Term), WorldTerm, Polarity * -1, Flags, Precedence);

1920

eml_SemiFunctTranslProp(term_FirstArgument(Term), WorldTerm, Polarity, Flags, Precedence);

1921

return Term;

1922

}

1923

/* Term = equiv(...) */

1924

else if (eml_IsEquivSymbol(Top)) {

1925

TERM termL, termR, termLneg, termRneg;

1926

termL = term_FirstArgument(Term);

1927

termR = term_SecondArgument(Term);

1928

termLneg = term_Create(fol_Not(), list_List(term_Copy(termL)));

1929

termRneg = term_Create(fol_Not(), list_List(term_Copy(termR)));

1930

if ( Polarity == 1 ) {

1931

term_RplacTop(Term, fol_And());

1932

list_Rplaca(term_ArgumentList(Term),

1933

term_Create(fol_Or(), list_Cons(termLneg, list_List(termR))));

1934

list_RplacSecond(term_ArgumentList(Term),

1935

term_Create(fol_Or(), list_Cons(termRneg, list_List(termL))));

1936

}

1937

else if (Polarity == -1) {

1938

term_RplacTop(Term, fol_Or());

1939

list_Rplaca(term_ArgumentList(Term),

1940

term_Create(fol_And(), list_Cons(termLneg, list_List(termRneg))));

1941

list_RplacSecond(term_ArgumentList(Term),

1942

term_Create(fol_And(), list_Cons(termL, list_List(termR))));

1943

}

1944

eml_SemiFunctTranslProp(Term, WorldTerm, Polarity, Flags, Precedence);

1945

return Term;

1946

}

1947

/* Term = or(...), Term = and(...) */

1948

/* must be tested after eml_IsNotSymbol, eml_IsImpliesSymbol amd eml_IsEquivSymbol */

1949

else if (eml_IsPropJunctor(Top)) {

1950

LIST Scan;

1951

for (Scan = term_ArgumentList(Term);

1952

!list_Empty(Scan);

1953

Scan = list_Cdr(Scan))

1954

eml_SemiFunctTranslProp(list_Car(Scan), WorldTerm, Polarity, Flags, Precedence);

1955

return Term;

1956

}

1957

else if (eml_IsModalOpSymbol(Top)) {

1958

/* Term = dia(alpha,phi), in the negation normal form (!) */

1959

if ( ( eml_IsDiaSymbol(Top) && (Polarity == 1) ) ||

1960

( eml_IsBoxSymbol(Top) && (Polarity == -1) ) ) {

1961

TERM newVar, newWorldTerm, relSubTerm, helpTerm, anotherHelpTerm;

1962

relSubTerm = term_FirstArgument(Term);

1963

newVar = term_Create(symbol_CreateStandardVariable(), list_Nil());

1964

newWorldTerm = term_Create(eml_ApplyFunct(),

1965

list_Cons(term_Copy(WorldTerm), list_List(newVar)));

1966

if (flag_GetFlagIntValue(Flags, flag_EMLFUNCNDEQ)) {

1967

helpTerm = eml_BuildSortQuantifierFor(Term, Top, term_TopSymbol(relSubTerm), term_TopSymbol(newVar), TRUE,

1968

list_List(eml_SemiFunctTranslProp(term_SecondArgument(Term),

1969

newWorldTerm, Polarity, Flags, Precedence)),

1970

(POINTER (*)())eml_CreateQuantifier, Precedence);

1971

list_Delete(term_ArgumentList(Term));

1972

anotherHelpTerm = eml_RplacWithOpAndArgs(Term, eml_FoJunctorAssocWithPropSymbol(Top),

1973

list_Cons(eml_SemiFunctTranslRelDia(relSubTerm, WorldTerm, Flags, Precedence),

1974

list_List(helpTerm)));

1975

term_Delete(newWorldTerm);

1976

return anotherHelpTerm;

1977

/* nde_r(w) /\ exists y_r tr(phi)(app(w,y_r)) */

1978

}

1979

else {

1980

helpTerm = term_Create(eml_FoJunctorAssocWithPropSymbol(Top),

1981

list_Cons(eml_SemiFunctTranslRelDia(relSubTerm, WorldTerm, Flags, Precedence),

1982

list_List(eml_SemiFunctTranslProp(term_SecondArgument(Term), newWorldTerm, Polarity, Flags, Precedence))));

1983

list_Delete(term_ArgumentList(Term));

1984

anotherHelpTerm = eml_BuildSortQuantifierFor(Term, Top, term_TopSymbol(relSubTerm),

1985

term_TopSymbol(newVar), TRUE,

1986

list_List(helpTerm), (POINTER (*)())eml_RplacWithQuantifier, Precedence);

1987

term_Delete(newWorldTerm);

1988

return anotherHelpTerm;

1989

/* exists y_r nde_r(w) /\ tr(phi)(app(w,y_r)) */

1990

}

1991

}

1992

/* Term = box(alpha,phi), in the negation normal form (!) */

1993

else {

1994

TERM newVar, helpTerm;

1995

newVar = term_Create(symbol_CreateStandardVariable(), list_Nil());

1996

helpTerm = term_Create(eml_FoJunctorAssocWithPropSymbol(Top),

1997

list_Cons(eml_SemiFunctTranslRelBox(term_FirstArgument(Term), WorldTerm, newVar, Flags, Precedence),

1998

list_List(eml_SemiFunctTranslProp(term_SecondArgument(Term), newVar, Polarity, Flags, Precedence))));

1999

list_Delete(term_ArgumentList(Term));

2000

return eml_RplacWithQuantifier(Term, eml_FoQuantAssocWithPropSymbol(Top), list_List(newVar),

2001

list_List(helpTerm));

2002

/* forall y tr(alpha)(w,y) -> tr(phi)(y) */

2003

}

2004

}

2005

else {

2006

fprintf(stderr, "\nNo case for %s in eml_SemiFunctTranslProp()\n",

2007

symbol_Name(Top));

2008

misc_Error();

2009

return NULL;

2010

}

2011

2012

}

2013

2014

2015

static TERM eml_SemiFunctTranslRelDia(TERM Term, TERM WorldTerm,

2016

FLAGSTORE Flags, PRECEDENCE Precedence)

2017

/**************************************************************

2018

INPUT: An eml (propositional) formula, argument term.

2019

RETURNS: Its semi functional translation.

2020

CAUTION: The term is destructively changed.

2021

***************************************************************/

2022

{

2023

SYMBOL Top;

2024

2025

Top = term_TopSymbol(Term);

2026

2027

/* Term = r */

2028

if (symbol_IsPredicate(Top)) {

2029

switch (flag_GetFlagIntValue(Flags, flag_EMLTHEORY)) {

2030

case flag_EMLTHEORYKD:

2031

return eml_RplacWithDesignatedPropAtom(Term, fol_True());

2032

break;

2033

case flag_EMLTHEORYK:

2034

return eml_RplacPropByFoAtom(Term, eml_SEMIFNDE, 1, list_List(term_Copy(WorldTerm)), Flags, Precedence);

2035

break;

2036

default:

2037

fprintf(stderr, "\nThe option EMLTheory = %d is not implemented in eml_SemiFunctTranslRel()\n",

2038

flag_GetFlagIntValue(Flags, flag_EMLTHEORY));

2039

misc_Error();

2040

return NULL;

2041

break;

2042

}

2043

}

2044

else {

2045

fprintf(stderr, "\nNo case for %s in eml_SemiFunctTranslRel()\n",

2046

symbol_Name(Top));

2047

misc_Error();

2048

return NULL;

2049

}

2050

}

2051

2052

static TERM eml_SemiFunctTranslRelBox(TERM Term, TERM WorldTerm, TERM VarY,

2053

FLAGSTORE Flags, PRECEDENCE Precedence)

2054

/**************************************************************

2055

INPUT: An eml (relational) formula, a term and a variable

2056

(the free variable).

2057

RETURNS: Its standard (relational) translation.

2058

CAUTION: The term is destructively changed.

2059

***************************************************************/

2060

{

2061

SYMBOL Top;

2062

2063

Top = term_TopSymbol(Term);

2064

2065

/* Term = r */

2066

if (symbol_IsPredicate(Top)) {

2067

return eml_RplacPropByFoAtom(Term, eml_REL, 2,

2068

list_Cons(term_Copy(WorldTerm), list_List(term_Copy(VarY))), Flags, Precedence);

2069

}

2070

else {

2071

fprintf(stderr, "\nNo case for %s in eml_SemiFunctTranslRelBox()\n",

2072

symbol_Name(Top));

2073

misc_Error();

2074

return NULL;

2075

}

2076

2077

}

2078

2079

2080

2081

static TERM eml_SemiFunctionalTranslation(TERM Term, int Polarity,

2082

FLAGSTORE Flags, PRECEDENCE Precedence)

2083

/**************************************************************

2084

INPUT: An eml (propositional) formula.

2085

RETURNS: Its semi functional translation.

2086

CAUTION: The term is destructively changed.

2087

***************************************************************/

2088

{

2089

TERM newVar, helpTerm;

2090

2091

symbol_ResetStandardVarCounter();

2092

2093

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

2094

printf("\n [SemiFuncTr] \t");

2095

newVar = term_Create(symbol_CreateStandardVariable(), list_Nil());

2096

helpTerm = eml_SemiFunctTranslProp(Term, newVar, Polarity, Flags, Precedence);

2097

return term_Create(fol_All(), list_Cons(term_Create(fol_Varlist(),list_List(newVar)), list_List(helpTerm)));

2098

/* forall x tr(Term,x) */

2099

2100

}

2101

2102

2103

2104

static TERM eml_RelFunctTranslProp(TERM Term, SYMBOL Var,

2105

char* SortEncoding, FLAGSTORE Flags, PRECEDENCE Precedence)

2106

/**************************************************************

2107

INPUT: An eml (propositional) formula, a variable, a string

2108

encoding of the sorts of the arguments and the modal depth.

2109

RETURNS: Its translation using the relational functional/path-based

2110

encoding of de Rijke et al.

2111

CAUTION: The term is destructively changed.

2112

***************************************************************/

2113

{

2114

SYMBOL Top;

2115

2116

Top = term_TopSymbol(Term);

2117

2118

/* Term = p */

2119

if (symbol_IsPredicate(Top)) {

2120

return eml_RplacPropByNaryAtom(Term, eml_PROP, SortEncoding,

2121

1, list_List(term_Create(Var,list_Nil())), Flags, Precedence);

2122

}

2123

/* Term = not(phi), Term = or(...) or Term = and(...) */

2124

else if (eml_IsPropJunctor(Top)) {

2125

LIST Scan;

2126

for (Scan=term_ArgumentList(Term); !list_Empty(Scan); Scan=list_Cdr(Scan))

2127

eml_RelFunctTranslProp(list_Car(Scan), Var,

2128

SortEncoding, Flags, Precedence);

2129

return Term;

2130

}

2131

/* Term = dia(r,phi) or Term = box(r,phi) */

2132

else if (eml_IsModalOpSymbol(Top)) {

2133

SYMBOL newVar;

2134

TERM helpTerm;

2135

SYMBOL relSubTop;

2136

char* newSortEncoding;

2137

int size;

2138

newVar = symbol_CreateStandardVariable();

2139

2140

relSubTop = term_TopSymbol(term_FirstArgument(Term));

2141

size = strlen(SortEncoding)+strlen(symbol_Name(relSubTop))+1;

2142

newSortEncoding = (char*)memory_Malloc(size*sizeof(char));

2143

sprintf(newSortEncoding,"%s%s", SortEncoding, symbol_Name(relSubTop));

2144

helpTerm = term_Create(eml_FoJunctorAssocWithPropSymbol(Top),

2145

list_Cons(eml_RelFunctTranslRel(term_FirstArgument(Term),Var,newVar,newSortEncoding, Flags, Precedence),

2146

list_List(eml_RelFunctTranslProp(term_SecondArgument(Term),newVar,newSortEncoding, Flags, Precedence))));

2147

list_Delete(term_ArgumentList(Term));

2148

memory_Free(newSortEncoding,size*sizeof(char));

2149

return eml_RplacWithQuantifier(Term, eml_FoQuantAssocWithPropSymbol(Top), list_List(term_Create(newVar,list_Nil())),

2150

list_List(helpTerm));

2151

/* exists y R_r(x,y) /\ tr(phi)(y) or

2152

* forall y R_r(x,y) -> tr(phi)(y) */

2153

}

2154

else {

2155

fprintf(stderr, "\nNo case for %s in eml_RelFunctTranslProp()\n",

2156

symbol_Name(Top));

2157

misc_Error();

2158

return NULL;

2159

}

2160

2161

}

2162

2163

static TERM eml_RelFunctTranslRel(TERM Term, SYMBOL VarX, SYMBOL VarY,

2164

char* SortEncoding, FLAGSTORE Flags, PRECEDENCE Precedence)

2165

/**************************************************************

2166

INPUT: An EML relational formula, a variable list, a string (encoding

2167

the sorts of the accessibility relations in the scope), and

2168

the length of the variable list (corresponds to the modal

2169

depth).

2170

RETURNS: Its functional translation ito n-ary predicates.

2171

CAUTION: The term is destructively changed.

2172

***************************************************************/

2173

{

2174

SYMBOL Top;

2175

2176

Top = term_TopSymbol(Term);

2177

2178

/* Term = r */

2179

if (symbol_IsPredicate(Top)) {

2180

switch (flag_GetFlagIntValue(Flags, flag_EMLTHEORY)) {

2181

case flag_EMLTHEORYK:

2182

return eml_RplacPropByNaryAtom(Term, eml_REL,

2183

SortEncoding, 2, list_Cons(term_Create(VarX,list_Nil()),list_List(term_Create(VarY,list_Nil()))), Flags, Precedence);

2184

break;

2185

default:

2186

fprintf(stderr, "\nThe option EMLTheory = %d is not implemented in eml_RelFunctTranslRel()\n",

2187

flag_GetFlagIntValue(Flags, flag_EMLTHEORY));

2188

misc_Error();

2189

return NULL;

2190

break;

2191

}

2192

}

2193

else {

2194

fprintf(stderr, "\nNo case for %s in eml_RelFunctTranslRel()\n",

2195

symbol_Name(Top));

2196

misc_Error();

2197

return NULL;

2198

}

2199

}

2200

2201

2202

2203

2204

static TERM eml_TranslateToFol(TERM Term, int Polarity,

2205

FLAGSTORE Flags, PRECEDENCE Precedence)

2206

/**************************************************************

2207

INPUT: An eml formula.

2208

RETURNS: Its translation as specified by flag_EMLTR, provided

2209

the formula is provided, otherwise the simplification of the

2210

original formula.

2211

CAUTION: The term is destructively changed.

2212

***************************************************************/

2213

{

2214

if (!eml_IsPropositional(Term))

2215

fol_NormalizeVars(Term);

2216

2217

Term = eml_ObviousSimplifications(Term, Flags);

2218

/* Term = eml_MakeOneAndOrCompSum(Term); */

2219

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

2220

printf("\n [Simpl]\t");

2221

if ( (Polarity == -1) ) { /* Conjecture */

2222

symbol_Print(fol_Not());

2223

putchar('(');

2224

/* printf("(not "); */

2225

/* putchar(' ');*/

2226

fol_PrintDFG(Term);

2227

printf(")");

2228

}

2229

else /* Axiom */

2230

fol_PrintDFG(Term);

2231

}

2232

2233

if (eml_IsPropositional(Term)) {

2234

switch (flag_GetFlagIntValue(Flags, flag_EMLTR)) {

2235

case flag_EMLTRREL:

2236

Term = eml_RelationalTranslation(Term, Flags, Precedence);

2237

break;

2238

case flag_EMLTRFUNC:

2239

case flag_EMLTROPTFUNC:

2240

Term = eml_FunctionalTranslation(Term, flag_GetFlagIntValue(Flags, flag_EMLFNARY), Flags, Precedence);

2241

break;

2242

case flag_EMLTRSEMIFUNC:

2243

Term = eml_SemiFunctionalTranslation(Term, Polarity, Flags, Precedence);

2244

break;

2245

default:

2246

fprintf(stderr, "\nFlag = %d is not implemented in eml_TranslateToFol()\n",

2247

flag_GetFlagIntValue(Flags, flag_EMLTR));

2248

misc_Error();

2249

break;

2250

}

2251

}

2252

else

2253

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

2254

printf("\n [FOL]\t");

2255

2256

return Term;

2257

}

2258

2259

static TERM eml_CreateTheoryTerm(int Flag, SYMBOL Symbol)

2260

/**************************************************************

2261

INPUT: A flag, must be of a logic determined by one axiom schema

2262

RETURNS: A single theory formula, e.g. for the flag flag_EMLTHEORYKD it

2263

returns forall x exists y R(x,y)

2264

REMARK: Prototypical. Only implemented for the relational

2265

translation and a few axiom schemas (D, T, B, 4, 5)

2266

***************************************************************/

2267

{

2268

TERM newVarX, newVarY, newVarZ, helpTerm;

2269

TERM term; /* theory formula */

2270

2271

switch (Flag) {

2272

2273

case flag_EMLTHEORYKD:

2274

/*printf("\nD");*/

2275

newVarX = term_Create(symbol_CreateStandardVariable(), list_Nil());

2276

newVarY = term_Create(symbol_CreateStandardVariable(), list_Nil());

2277

term = term_Create(Symbol, /* R(x,y) */

2278

list_Nconc(list_List(newVarX), list_List(newVarY)));

2279

/*printf("\n [*]\t"); fol_PrintDFG(term);*/

2280

helpTerm = term_Create(fol_Exist(), /* exists y R(x,y) */

2281

list_Cons(term_Create(fol_Varlist(), list_List(term_Copy(newVarY))),

2282

list_List(term)));

2283

/*printf("\n [**]\t"); fol_PrintDFG(helpTerm);*/

2284

term = term_Create(fol_All(), /* forall x exists y R(x,y) */

2285

list_Cons(term_Create(fol_Varlist(), list_List(term_Copy(newVarX))),

2286

list_List(helpTerm) ));

2287

/*printf("\n [***]\t"); fol_PrintDFG(term);*/

2288

return term;

2289

break;

2290

2291

case flag_EMLTHEORYKT:

2292

/*printf("\nT");*/

2293

newVarX = term_Create(symbol_CreateStandardVariable(), list_Nil());

2294

helpTerm = term_Create(Symbol, /* R(x,x) */

2295

list_Nconc(list_List(newVarX), list_List(term_Copy(newVarX))));

2296

/*printf("\n [*]\t"); fol_PrintDFG(helpTerm);*/

2297

term = term_Create(fol_All(), /* forall x R(x,x) */

2298

list_Cons(term_Create(fol_Varlist(), list_List(term_Copy(newVarX))),

2299

list_List(helpTerm) ));

2300

return term;

2301

break;

2302

2303

case flag_EMLTHEORYKB:

2304

/*printf("\nB");*/

2305

newVarX = term_Create(symbol_CreateStandardVariable(), list_Nil());

2306

newVarY = term_Create(symbol_CreateStandardVariable(), list_Nil());

2307

term = term_Create(Symbol, /* R(x,y) */

2308

list_Nconc(list_List(newVarX), list_List(newVarY)));

2309

/*printf("\n [*]\t"); fol_PrintDFG(term);*/

2310

helpTerm = term_Create(Symbol, /* R(y,x) */

2311

list_Nconc(list_List(term_Copy(newVarY)), list_List(term_Copy(newVarX))));

2312

/*printf("\n [**]\t"); fol_PrintDFG(helpTerm);*/

2313

helpTerm = term_Create(fol_Implies(), /* R(x,y) -> R(y,x) */

2314

list_Cons(term, list_List(helpTerm)));

2315

/*printf("\n [***]\t"); fol_PrintDFG(helpTerm);*/

2316

term = term_Create(fol_All(), /* forall x y R(x,y) -> R(y,x) */

2317

list_Cons(term_Create(fol_Varlist(),

2318

list_Cons(term_Copy(newVarX), list_List(term_Copy(newVarY)))),

2319

list_List(helpTerm) ));

2320

/*printf("\n [****]\t"); fol_PrintDFG(term);*/

2321

return term;

2322

break;

2323

2324

case flag_EMLTHEORYK4:

2325

/*printf("\n4");*/

2326

newVarX = term_Create(symbol_CreateStandardVariable(), list_Nil());

2327

newVarY = term_Create(symbol_CreateStandardVariable(), list_Nil());

2328

newVarZ = term_Create(symbol_CreateStandardVariable(), list_Nil());

2329

term = term_Create(Symbol, /* R(x,y) */

2330

list_Nconc(list_List(newVarX), list_List(newVarY)));

2331

/*printf("\n [*]\t"); fol_PrintDFG(term);*/

2332

helpTerm = term_Create(Symbol, /* R(y,z) */

2333

list_Nconc(list_List(term_Copy(newVarY)), list_List(newVarZ)));

2334

/*printf("\n [**]\t"); fol_PrintDFG(helpTerm);*/

2335

helpTerm = term_Create(fol_And(), /* R(x,y) /\ R(y,z) */

2336

list_Cons(term, list_List(helpTerm)));

2337

/*printf("\n [***]\t"); fol_PrintDFG(helpTerm);*/

2338

term = term_Create(Symbol, /* R(x,z) */

2339

list_Nconc(list_List(term_Copy(newVarX)), list_List(term_Copy(newVarZ))));

2340

/*printf("\n [****]\t"); fol_PrintDFG(term);*/

2341

helpTerm = term_Create(fol_Implies(), /* (R(x,y) /\ R(y,z)) -> R(x,z) */

2342

list_Cons(helpTerm, list_List(term)));

2343

/*printf("\n [*****]\t"); fol_PrintDFG(helpTerm);*/

2344

term = term_Create(fol_All(), /* forall x y z (R(x,y) /\ R(y,z)) -> R(x,z) */

2345

list_Cons(term_Create(fol_Varlist(),

2346

list_Cons(term_Copy(newVarX),

2347

list_Cons(term_Copy(newVarY),

2348

list_List(term_Copy(newVarZ))))),

2349

list_List(helpTerm) ));

2350

/*printf("\n [******]\t"); fol_PrintDFG(term);*/

2351

return term;

2352

break;

2353

2354

case flag_EMLTHEORYK5:

2355

/*printf("\n5");*/

2356

newVarX = term_Create(symbol_CreateStandardVariable(), list_Nil());

2357

newVarY = term_Create(symbol_CreateStandardVariable(), list_Nil());

2358

newVarZ = term_Create(symbol_CreateStandardVariable(), list_Nil());

2359

term = term_Create(Symbol, /* R(x,y) */

2360

list_Nconc(list_List(newVarX), list_List(newVarY)));

2361

/*printf("\n [*]\t"); fol_PrintDFG(term);*/

2362

helpTerm = term_Create(Symbol, /* R(x,z) */

2363

list_Nconc(list_List(term_Copy(newVarX)), list_List(newVarZ)));

2364

/*printf("\n [**]\t"); fol_PrintDFG(helpTerm);*/

2365

helpTerm = term_Create(fol_And(), /* R(x,y) /\ R(x,z) */

2366

list_Cons(term, list_List(helpTerm)));

2367

/*printf("\n [***]\t"); fol_PrintDFG(helpTerm);*/

2368

term = term_Create(Symbol, /* R(y,z) */

2369

list_Nconc(list_List(term_Copy(newVarY)), list_List(term_Copy(newVarZ))));

2370

/*printf("\n [****]\t"); fol_PrintDFG(term);*/

2371

helpTerm = term_Create(fol_Implies(), /* (R(x,y) /\ R(x,z)) -> R(y,z) */

2372

list_Cons(helpTerm, list_List(term)));

2373

/*printf("\n [*****]\t"); fol_PrintDFG(helpTerm);*/

2374

term = term_Create(fol_All(), /* forall x y z (R(x,y) /\ R(x,z)) -> R(y,z) */

2375

list_Cons(term_Create(fol_Varlist(),

2376

list_Cons(term_Copy(newVarX),

2377

list_Cons(term_Copy(newVarY),

2378

list_List(term_Copy(newVarZ))))),

2379

list_List(helpTerm) ));

2380

/*printf("\n [******]\t"); fol_PrintDFG(term);*/

2381

return term;

2382

break;

2383

2384

default:

2385

fprintf(stderr, "\nFlag = %d is not implemented in eml_CreateTheoryTerm()\n",

2386

Flag);

2387

misc_Error();

2388

return NULL;

2389

}

2390

}

2391

2392

static void eml_AddBackgroundTheory(LIST* Axiomlist, FLAGSTORE Flags)

2393

/**************************************************************

2394

INPUT: The list of axioms

2395

RETURNS: Nothing

2396

EFFECT: Additional axioms may be added to the list of axioms.

2397

REMARK: Prototypical. Only implemented for the relational

2398

translation and a few logics (K, KD, KT, KB, K4, K5, S4, S5 )

2399

***************************************************************/

2400

{

2401

int i, flag;

2402

char L[100];

2403

char* label;

2404

SYMBOL symbol;

2405

LIST pair = list_Nil(); /* theory formula plus label */

2406

LIST theory = list_Nil(); /* list of theory formulae */

2407

2408

/*printf("\n Beginning of eml_AddBackgroundTheory()\t");*/

2409

2410

if ( (flag_GetFlagIntValue(Flags, flag_EMLTHEORY) != flag_EMLTHEORYK) &&

2411

(flag_GetFlagIntValue(Flags, flag_EMLTR) == flag_EMLTRREL) ) {

2412

2413

for (i = 1; i < symbol_ActIndex(); i++) {

2414

if (!symbol_IsFreed(i)) {

2415

symbol = symbol_Signature(i)->info;

2416

/* printf("\n []\t"); symbol_Print(symbol); */

2417

if ( symbol_IsPredicate(symbol) &&

2418

(symbol_Signature(i)->arity == 2) &&

2419

!symbol_Equal(symbol, fol_Equality())) {

2420

flag = flag_GetFlagIntValue(Flags, flag_EMLTHEORY);

2421

switch (flag) {

2422

2423

case flag_EMLTHEORYKD:

2424

case flag_EMLTHEORYKT:

2425

case flag_EMLTHEORYKB:

2426

case flag_EMLTHEORYK4:

2427

case flag_EMLTHEORYK5:

2428

sprintf(L,"%s%s", eml_RELPROPERTYLABELS[flag], symbol_Name(symbol));

2429

label = memory_Malloc(sizeof(char) * (strlen(L) + 1));

2430

sprintf(label, "%s", L);

2431

pair = list_PairCreate(label, eml_CreateTheoryTerm(flag, symbol));

2432

/*printf("\nLabel : %s", (char*) list_PairFirst(pair)); */

2433

/*printf("\nTheory formula : "); fol_PrintDFG(list_PairSecond(pair));*/

2434

theory = list_Nconc(theory, list_List(pair));

2435

break;

2436

2437

case flag_EMLTHEORYS4:

2438

/* T / reflexivity */

2439

sprintf(L,"%s%s", eml_RELPROPERTYLABELS[flag_EMLTHEORYKT], symbol_Name(symbol));

2440

label = memory_Malloc(sizeof(char) * (strlen(L) + 1));

2441

sprintf(label, "%s", L);

2442

pair = list_PairCreate(label, eml_CreateTheoryTerm(flag_EMLTHEORYKT, symbol));

2443

/*printf("\nLabel : %s", (char*) list_PairFirst(pair)); */

2444

/*printf("\nTheory formula : "); fol_PrintDFG(list_PairSecond(pair));*/

2445

theory = list_Nconc(theory, list_List(pair));

2446

/* 4 / transitivity */

2447

sprintf(L,"%s%s", eml_RELPROPERTYLABELS[flag_EMLTHEORYK4], symbol_Name(symbol));

2448

label = memory_Malloc(sizeof(char) * (strlen(L) + 1));

2449

sprintf(label, "%s", L);

2450

pair = list_PairCreate(label, eml_CreateTheoryTerm(flag_EMLTHEORYK4, symbol));

2451

/*printf("\nLabel : %s", (char*) list_PairFirst(pair)); */

2452

/*printf("\nTheory formula : "); fol_PrintDFG(list_PairSecond(pair));*/

2453

theory = list_Nconc(theory, list_List(pair));

2454

break;

2455

2456

case flag_EMLTHEORYS5:

2457

/* T / reflexivity */

2458

sprintf(L,"%s%s", eml_RELPROPERTYLABELS[flag_EMLTHEORYKT], symbol_Name(symbol));

2459

label = memory_Malloc(sizeof(char) * (strlen(L) + 1));

2460

sprintf(label, "%s", L);

2461

pair = list_PairCreate(label, eml_CreateTheoryTerm(flag_EMLTHEORYKT, symbol));

2462

/*printf("\nLabel : %s", (char*) list_PairFirst(pair)); */

2463

/*printf("\nTheory formula : "); fol_PrintDFG(list_PairSecond(pair));*/

2464

theory = list_Nconc(theory, list_List(pair));

2465

/* B / symmetry */

2466

sprintf(L,"%s%s", eml_RELPROPERTYLABELS[flag_EMLTHEORYKB], symbol_Name(symbol));

2467

label = memory_Malloc(sizeof(char) * (strlen(L) + 1));

2468

sprintf(label, "%s", L);

2469

pair = list_PairCreate(label, eml_CreateTheoryTerm(flag_EMLTHEORYKB, symbol));

2470

/*printf("\nLabel : %s", (char*) list_PairFirst(pair)); */

2471

/*printf("\nTheory formula : "); fol_PrintDFG(list_PairSecond(pair));*/

2472

theory = list_Nconc(theory, list_List(pair));

2473

/* 4 / transitivity */

2474

sprintf(L,"%s%s", eml_RELPROPERTYLABELS[flag_EMLTHEORYK4], symbol_Name(symbol));

2475

label = memory_Malloc(sizeof(char) * (strlen(L) + 1));

2476

sprintf(label, "%s", L);

2477

pair = list_PairCreate(label, eml_CreateTheoryTerm(flag_EMLTHEORYK4, symbol));

2478

/*printf("\nLabel : %s", (char*) list_PairFirst(pair)); */

2479

/*printf("\nTheory formula : "); fol_PrintDFG(list_PairSecond(pair));*/

2480

theory = list_Nconc(theory, list_List(pair));

2481

break;

2482

default:

2483

fprintf(stderr, "\nThe option EMLTheory = %d is not implemented in eml_AddBackgroundTheory()\n",

2484

flag_GetFlagIntValue(Flags, flag_EMLTHEORY));

2485

misc_Error();

2486

break;

2487

}

2488

#ifdef DEBUG

2489

if (list_Empty(theory)) {

2490

fprintf(stderr, "In eml_AddBackgroundTheory(): theory is empty\n");

2491

misc_Error();

2492

}

2493

if (list_Empty(*Axiomlist)) {

2494

fprintf(stderr, "In eml_AddBackgroundTheory(): *Axiomlist is empty\n");

2495

misc_Error();

2496

}

2497

#endif

2498

}

2499

}

2500

}

2501

*Axiomlist = list_Nconc(theory, *Axiomlist);

2502

}

2503

}

2504

2505

2506

void eml_TranslateToFolMain(LIST* AxiomList, LIST* ConjectureList,

2507

BOOL KeepProofSearch, FLAGSTORE Flags, PRECEDENCE Precedence)

2508

/**************************************************************

2509

INPUT: A list of axiom formulae,

2510

a list of conjecture formulae,

2511

a hasharray in which for every clause the list of labels

2512

of the terms used for deriving the clause is stored (if DocProof

2513

is set),

2514

a flag store

2515

RETURNS: If KeepProofSearch is TRUE, then the ProofSearch object is not

2516

freed but returned.

2517

Else, NULL is returned.

2518

***************************************************************/

2519

{

2520

LIST Scan, Pair;

2521

TERM helpTerm;

2522

int flag_emltr;

2523

2524

/* NOTE: EMLAUTO mode not as yet implemented */

2525

2526

/* Print warnings for non-sensical flag combinations */

2527

flag_emltr = flag_GetFlagIntValue(Flags, flag_EMLTR);

2528

if (flag_GetFlagIntValue(Flags, flag_DOCPROOF) || flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

2529

flag_CheckEmlTranslationFlags(Flags, flag_emltr);

2530

}

2531

2532

/* Set additional flags */

2533

if (flag_emltr == flag_EMLTROPTFUNC) {

2534

flag_SetFlagIntValue(Flags, flag_CNFQUANTEXCH, flag_CNFQUANTEXCHON);

2535

}

2536

/* This caused a memory leak because of the allocation done in

2537

* cnf_Init; fixed with warnings

2538

* if (flag_GetFlagIntValue(Flags, flag_CNFQUANTEXCH)) {

2539

flag_SetFlagIntValue(Flags, flag_CNFOPTSKOLEM, flag_CNFOPTSKOLEMOFF);

2540

flag_SetFlagIntValue(Flags, flag_CNFSTRSKOLEM, flag_CNFSTRSKOLEMOFF);

2541

} */

2542

/*

2543

if ((flag_emltr == flag_EMLTRFUNC || flag_emltr == flag_EMLTROPTFUNC) &&

2544

flag_GetFlagIntValue(Flags, flag_EMLFFSORTS)) {

2545

flag_SetFlagIntValue(Flags, flag_SORTS, flag_SORTSMONADICWITHVARIABLE);

2546

} */

2547

/* RS: Check with Christoph?? */

2548

2549

/* Limitations of current implementation */

2550

Scan = *AxiomList;

2551

if ( !list_Empty(Scan) && !list_Empty(list_Car(Scan)) ) {

2552

if ( flag_emltr == flag_EMLTROPTFUNC ) {

2553

fprintf(stderr, "ERROR: With the current implementation of the translation routines\n");

2554

fprintf(stderr, " no axioms are allowed when the optimised functional translation\n");

2555

fprintf(stderr, " is used (EMLTranslation=2)\n");

2556

misc_Error();

2557

}

2558

else {

2559

if ( flag_GetFlagIntValue(Flags, flag_EMLFNARY) ) {

2560

fprintf(stderr, "ERROR: With the current implementation of the translation routines\n");

2561

fprintf(stderr, " no axioms are allowed when the encoding is in terms of\n");

2562

fprintf(stderr, " n-ary predicates (EMLFuncNary=1)\n");

2563

misc_Error();

2564

}

2565

}

2566

}

2567

2568

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

2569

printf("\n--------------------EML-TRANSLATION-START-------------------------");

2570

printf("\n Special : ");

2571

flag_PrintEmlTranslationMethod(flag_emltr);

2572

flag_PrintEmlTranslationFlags(Flags);

2573

printf("\n Precedence: "); symbol_PrintPrecedence(Precedence);

2574

printf("\nAxioms:");

2575

}

2576

2577

/* Initialisation */

2578

switch (flag_GetFlagIntValue(Flags, flag_EMLTR)) {

2579

case flag_EMLTRFUNC:

2580

case flag_EMLTROPTFUNC:

2581

case flag_EMLTRSEMIFUNC:

2582

eml_InitFunctTransl(Flags, Precedence);

2583

break;

2584

default:

2585

/* Do nothing */

2586

break;

2587

}

2588

2589

for(Scan=*AxiomList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {

2590

Pair = list_Car(Scan);

2591

helpTerm = (TERM) list_PairSecond(Pair);

2592

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

2593

if ( !list_Empty(list_PairFirst(Pair)) ) {

2594

printf("\nLabel : %s", (char*) list_PairFirst(Pair));

2595

}

2596

if (eml_IsPropositional(helpTerm))

2597

printf("\n [%s]\t", flag_Name(flag_EML));

2598

else

2599

printf("\n [FOL]\t");

2600

fol_PrintDFG(helpTerm);

2601

}

2602

helpTerm = eml_TranslateToFol(helpTerm, 1, Flags, Precedence);

2603

/* positive polarity */

2604

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

2605

fol_PrintDFG(helpTerm);

2606

printf("\n");

2607

}

2608

list_Rplacd(Pair, (LIST) helpTerm);

2609

}

2610

2611

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

2612

printf("\n\nConjecture:");

2613

2614

for(Scan=*ConjectureList; !list_Empty(Scan); Scan = list_Cdr(Scan)) {

2615

Pair = list_Car(Scan);

2616

helpTerm = (TERM) list_PairSecond(Pair);

2617

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

2618

if ( !list_Empty(list_PairFirst(Pair)) ) {

2619

printf("\nLabel : %s", (char*) list_PairFirst(Pair));

2620

}

2621

if (eml_IsPropositional(helpTerm))

2622

printf("\n [%s]\t", flag_Name(flag_EML));

2623

else

2624

printf("\n [FOL]\t");

2625

fol_PrintDFG(helpTerm);

2626

}

2627

#ifdef DEBUG

2628

if (!symbol_Equal(term_TopSymbol(helpTerm),fol_Not())) {

2629

fprintf(stderr, "In eml_TranslateToFolMain(): The list of conjectures should have been negated\n");

2630

misc_Error();

2631

}

2632

#endif

2633

2634

term_RplacFirstArgument(helpTerm,

2635

eml_TranslateToFol(term_FirstArgument(helpTerm), -1, Flags, Precedence));

2636

/* negative polarity */

2637

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS)) {

2638

fol_PrintDFG(helpTerm);

2639

}

2640

list_Rplacd(Pair, (LIST) helpTerm);

2641

}

2642

if (flag_GetFlagIntValue(Flags, flag_EMLPTRANS))

2643

printf("\n");

2644

2645

eml_AddBackgroundTheory(AxiomList, Flags);

2646

2647

/* Check whether the following does the job (as it is supposed to).

2648

* Deleting the symbol list causes a segmentation fault later on in cnf.c.

2649

* Is this possbily due to a missing

2650

* if (!list_PointerMember(symbol_FREEDSYMBOLS,(POINTER)Index))

2651

* ??

2652

* */

2653

}