GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/tptp/tptp.cpp Lines: 185 231 80.1 %
Date: 2021-03-23 Branches: 255 718 35.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file tptp.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Francois Bobot, Haniel Barbosa
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Definitions of TPTP constants.
13
 **
14
 ** Definitions of TPTP constants.
15
 **/
16
17
// Do not #include "parser/antlr_input.h" directly. Rely on the header.
18
#include "parser/tptp/tptp.h"
19
20
#include <algorithm>
21
#include <set>
22
23
#include "api/cvc4cpp.h"
24
#include "base/check.h"
25
#include "options/options.h"
26
#include "parser/parser.h"
27
#include "smt/command.h"
28
29
// ANTLR defines these, which is really bad!
30
#undef true
31
#undef false
32
33
namespace CVC4 {
34
namespace parser {
35
36
42
Tptp::Tptp(api::Solver* solver,
37
           SymbolManager* sm,
38
           Input* input,
39
           bool strictMode,
40
42
           bool parseOnly)
41
    : Parser(solver, sm, input, strictMode, parseOnly),
42
      d_cnf(false),
43
42
      d_fof(false)
44
{
45
42
  addTheory(Tptp::THEORY_CORE);
46
47
  /* Try to find TPTP dir */
48
  // From tptp4x FileUtilities
49
  //----Try the TPTP directory, and TPTP variations
50
42
  char* home = getenv("TPTP");
51
42
  if(home == NULL) {
52
42
     home = getenv("TPTP_HOME");
53
// //----If no TPTP_HOME, try the tptp user (aaargh)
54
//         if(home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) {
55
//            home = PasswdEntry->pw_dir;
56
//         }
57
//----Now look in the TPTP directory from there
58
42
    if(home != NULL) {
59
      d_tptpDir = home;
60
      d_tptpDir.append("/TPTP/");
61
    }
62
  } else {
63
    d_tptpDir = home;
64
    //add trailing "/"
65
    if(d_tptpDir[d_tptpDir.size() - 1] != '/') {
66
      d_tptpDir.append("/");
67
    }
68
  }
69
42
  d_hasConjecture = false;
70
42
}
71
72
126
Tptp::~Tptp() {
73
49
  for( unsigned i=0; i<d_in_created.size(); i++ ){
74
7
    d_in_created[i]->free(d_in_created[i]);
75
  }
76
84
}
77
78
42
void Tptp::addTheory(Theory theory) {
79
42
  switch(theory) {
80
42
  case THEORY_CORE:
81
    //TPTP (CNF and FOF) is unsorted so we define this common type
82
    {
83
84
      std::string d_unsorted_name = "$$unsorted";
84
42
      d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name);
85
84
      preemptCommand(new DeclareSortCommand(d_unsorted_name, 0, d_unsorted));
86
    }
87
    // propositionnal
88
42
    defineType("Bool", d_solver->getBooleanSort());
89
42
    defineVar("$true", d_solver->mkTrue());
90
42
    defineVar("$false", d_solver->mkFalse());
91
42
    addOperator(api::AND);
92
42
    addOperator(api::EQUAL);
93
42
    addOperator(api::IMPLIES);
94
    // addOperator(api::ITE); //only for tff thf
95
42
    addOperator(api::NOT);
96
42
    addOperator(api::OR);
97
42
    addOperator(api::XOR);
98
42
    addOperator(api::APPLY_UF);
99
    //Add quantifiers?
100
42
    break;
101
102
  default:
103
    std::stringstream ss;
104
    ss << "internal error: Tptp::addTheory(): unhandled theory " << theory;
105
    throw ParserException(ss.str());
106
  }
107
42
}
108
109
110
/* The include are managed in the lexer but called in the parser */
111
// Inspired by http://www.antlr3.org/api/C/interop.html
112
113
7
bool newInputStream(std::string fileName, pANTLR3_LEXER lexer, std::vector< pANTLR3_INPUT_STREAM >& inc ) {
114
7
  Debug("parser") << "Including " << fileName << std::endl;
115
  // Create a new input stream and take advantage of built in stream stacking
116
  // in C target runtime.
117
  //
118
  pANTLR3_INPUT_STREAM    in;
119
#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
120
  in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) fileName.c_str());
121
#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
122
7
  in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT);
123
#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
124
7
  if(in == NULL) {
125
    Debug("parser") << "Can't open " << fileName << std::endl;
126
    return false;
127
  }
128
  // Same thing as the predefined PUSHSTREAM(in);
129
7
  lexer->pushCharStream(lexer,in);
130
  // restart it
131
  //lexer->rec->state->tokenStartCharIndex  = -10;
132
  //lexer->emit(lexer);
133
134
  // Note that the input stream is not closed when it EOFs, I don't bother
135
  // to do it here, but it is up to you to track streams created like this
136
  // and destroy them when the whole parse session is complete. Remember that you
137
  // don't want to do this until all tokens have been manipulated all the way through
138
  // your tree parsers etc as the token does not store the text it just refers
139
  // back to the input stream and trying to get the text for it will abort if you
140
  // close the input stream too early.
141
  //
142
7
  inc.push_back( in );
143
144
  //TODO what said before
145
7
  return true;
146
}
147
148
7
void Tptp::includeFile(std::string fileName) {
149
  // security for online version
150
7
  if(!canIncludeFile()) {
151
    parseError("include-file feature was disabled for this run.");
152
  }
153
154
  // Get the lexer
155
7
  AntlrInput * ai = static_cast<AntlrInput *>(getInput());
156
7
  pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
157
158
  // push the inclusion scope; will be popped by our special popCharStream
159
  // would be necessary for handling symbol filtering in inclusions
160
  //pushScope();
161
162
  // get the name of the current stream "Does it work inside an include?"
163
7
  const std::string inputName = ai->getInputStreamName();
164
165
  // Test in the directory of the actual parsed file
166
7
  std::string currentDirFileName;
167
7
  if(inputName != "<stdin>") {
168
    // TODO: Use dirname or Boost::filesystem?
169
7
    size_t pos = inputName.rfind('/');
170
7
    if(pos != std::string::npos) {
171
      currentDirFileName = std::string(inputName, 0, pos + 1);
172
    }
173
7
    currentDirFileName.append(fileName);
174
7
    if(newInputStream(currentDirFileName,lexer, d_in_created)) {
175
7
      return;
176
    }
177
  } else {
178
    currentDirFileName = "<unknown current directory for stdin>";
179
  }
180
181
  if(d_tptpDir.empty()) {
182
    parseError("Couldn't open included file: " + fileName
183
               + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
184
  };
185
186
  std::string tptpDirFileName = d_tptpDir + fileName;
187
  if(! newInputStream(tptpDirFileName,lexer, d_in_created)) {
188
    parseError("Couldn't open included file: " + fileName
189
               + " at " + currentDirFileName + " or " + tptpDirFileName);
190
  }
191
}
192
193
3
void Tptp::checkLetBinding(const std::vector<api::Term>& bvlist,
194
                           api::Term lhs,
195
                           api::Term rhs,
196
                           bool formula)
197
{
198
3
  if (lhs.getKind() != api::APPLY_UF)
199
  {
200
    parseError("malformed let: LHS must be a flat function application");
201
  }
202
6
  const std::multiset<api::Term> vars{lhs.begin(), lhs.end()};
203
3
  if (formula && !lhs.getSort().isBoolean())
204
  {
205
    parseError("malformed let: LHS must be formula");
206
  }
207
11
  for (const CVC4::api::Term& var : vars)
208
  {
209
8
    if (var.hasOp())
210
    {
211
      parseError("malformed let: LHS must be flat, illegal child: " +
212
                 var.toString());
213
    }
214
  }
215
216
  // ensure all let-bound variables appear on the LHS, and appear only once
217
8
  for (const api::Term& bound_var : bvlist)
218
  {
219
5
    const size_t count = vars.count(bound_var);
220
5
    if (count == 0) {
221
      parseError(
222
          "malformed let: LHS must make use of all quantified variables, "
223
          "missing `" +
224
          bound_var.toString() + "'");
225
5
    } else if (count >= 2) {
226
      parseError("malformed let: LHS cannot use same bound variable twice: " +
227
                 bound_var.toString());
228
    }
229
  }
230
3
}
231
232
5258
api::Term Tptp::parseOpToExpr(ParseOp& p)
233
{
234
10516
  api::Term expr;
235
5258
  if (!p.d_expr.isNull())
236
  {
237
    return p.d_expr;
238
  }
239
  // if it has a kind, it's a builtin one and this function should not have been
240
  // called
241
5258
  Assert(p.d_kind == api::NULL_EXPR);
242
5258
  if (isDeclared(p.d_name))
243
  {  // already appeared
244
5174
    expr = getVariable(p.d_name);
245
  }
246
  else
247
  {
248
    api::Sort t =
249
168
        p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
250
84
    expr = bindVar(p.d_name, t, true);  // must define at level zero
251
84
    preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
252
  }
253
5258
  return expr;
254
}
255
256
895
api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
257
{
258
895
  if (Debug.isOn("parser"))
259
  {
260
    Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
261
    for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
262
         ++i)
263
    {
264
      Debug("parser") << "++ " << *i << std::endl;
265
    }
266
  }
267
895
  Assert(!args.empty());
268
  // If operator already defined, just build application
269
895
  if (!p.d_expr.isNull())
270
  {
271
    // this happens with some arithmetic kinds, which are wrapped around
272
    // lambdas.
273
27
    args.insert(args.begin(), p.d_expr);
274
27
    return d_solver->mkTerm(api::APPLY_UF, args);
275
  }
276
868
  bool isBuiltinKind = false;
277
  // the builtin kind of the overall return expression
278
868
  api::Kind kind = api::NULL_EXPR;
279
  // First phase: piece operator together
280
868
  if (p.d_kind == api::NULL_EXPR)
281
  {
282
    // A non-built-in function application, get the expression
283
1010
    api::Term v;
284
505
    if (isDeclared(p.d_name))
285
    {  // already appeared
286
439
      v = getVariable(p.d_name);
287
    }
288
    else
289
    {
290
132
      std::vector<api::Sort> sorts(args.size(), d_unsorted);
291
      api::Sort t =
292
132
          p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
293
66
      t = d_solver->mkFunctionSort(sorts, t);
294
66
      v = bindVar(p.d_name, t, true);  // must define at level zero
295
66
      preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
296
    }
297
    // args might be rationals, in which case we need to create
298
    // distinct constants of the "unsorted" sort to represent them
299
1213
    for (size_t i = 0; i < args.size(); ++i)
300
    {
301
2124
      if (args[i].getSort().isReal()
302
2124
          && v.getSort().getFunctionDomainSorts()[i] == d_unsorted)
303
      {
304
        args[i] = convertRatToUnsorted(args[i]);
305
      }
306
    }
307
505
    Assert(!v.isNull());
308
505
    checkFunctionLike(v);
309
505
    kind = getKindForFunction(v);
310
505
    args.insert(args.begin(), v);
311
  }
312
  else
313
  {
314
363
    kind = p.d_kind;
315
363
    isBuiltinKind = true;
316
  }
317
868
  Assert(kind != api::NULL_EXPR);
318
868
  const Options& opts = d_solver->getOptions();
319
  // Second phase: apply parse op to the arguments
320
868
  if (isBuiltinKind)
321
  {
322
363
    if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
323
    {
324
      // need --uf-ho if these operators are applied over function args
325
201
      for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
326
           ++i)
327
      {
328
134
        if ((*i).getSort().isFunction())
329
        {
330
          parseError(
331
              "Cannot apply equalty to functions unless --uf-ho is set.");
332
        }
333
      }
334
    }
335
1089
    if (!strictModeEnabled() && (kind == api::AND || kind == api::OR)
336
425
        && args.size() == 1)
337
    {
338
      // Unary AND/OR can be replaced with the argument.
339
      return args[0];
340
    }
341
363
    if (kind == api::MINUS && args.size() == 1)
342
    {
343
      return d_solver->mkTerm(api::UMINUS, args[0]);
344
    }
345
363
    return d_solver->mkTerm(kind, args);
346
  }
347
348
  // check if partially applied function, in this case we use HO_APPLY
349
505
  if (args.size() >= 2)
350
  {
351
1010
    api::Sort argt = args[0].getSort();
352
505
    if (argt.isFunction())
353
    {
354
505
      unsigned arity = argt.getFunctionArity();
355
505
      if (args.size() - 1 < arity)
356
      {
357
        if (!opts.getUfHo())
358
        {
359
          parseError("Cannot partially apply functions unless --uf-ho is set.");
360
        }
361
        Debug("parser") << "Partial application of " << args[0];
362
        Debug("parser") << " : #argTypes = " << arity;
363
        Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
364
        // must curry the partial application
365
        return d_solver->mkTerm(api::HO_APPLY, args);
366
      }
367
    }
368
  }
369
505
  return d_solver->mkTerm(kind, args);
370
}
371
372
1
void Tptp::forceLogic(const std::string& logic)
373
{
374
1
  Parser::forceLogic(logic);
375
1
  preemptCommand(new SetBenchmarkLogicCommand(logic));
376
1
}
377
378
59
void Tptp::addFreeVar(api::Term var)
379
{
380
59
  Assert(cnf());
381
59
  d_freeVar.push_back(var);
382
59
}
383
384
85
std::vector<api::Term> Tptp::getFreeVar()
385
{
386
85
  Assert(cnf());
387
85
  std::vector<api::Term> r;
388
85
  r.swap(d_freeVar);
389
85
  return r;
390
}
391
392
42
api::Term Tptp::convertRatToUnsorted(api::Term expr)
393
{
394
  // Create the conversion function If they doesn't exists
395
42
  if (d_rtu_op.isNull()) {
396
12
    api::Sort t;
397
    // Conversion from rational to unsorted
398
6
    t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted);
399
6
    d_rtu_op = d_solver->mkConst(t, "$$rtu");
400
6
    preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
401
    // Conversion from unsorted to rational
402
6
    t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort());
403
6
    d_utr_op = d_solver->mkConst(t, "$$utr");
404
6
    preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
405
  }
406
  // Add the inverse in order to show that over the elements that
407
  // appear in the problem there is a bijection between unsorted and
408
  // rational
409
84
  api::Term ret = d_solver->mkTerm(api::APPLY_UF, d_rtu_op, expr);
410
42
  if (d_r_converted.find(expr) == d_r_converted.end()) {
411
30
    d_r_converted.insert(expr);
412
30
    api::Term eq = d_solver->mkTerm(
413
60
        api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret));
414
30
    preemptCommand(new AssertCommand(eq));
415
  }
416
84
  return api::Term(ret);
417
}
418
419
6
api::Term Tptp::convertStrToUnsorted(std::string str)
420
{
421
6
  api::Term& e = d_distinct_objects[str];
422
6
  if (e.isNull())
423
  {
424
6
    e = d_solver->mkConst(d_unsorted, str);
425
  }
426
6
  return e;
427
}
428
429
1
api::Term Tptp::mkLambdaWrapper(api::Kind k, api::Sort argType)
430
{
431
2
  Debug("parser") << "mkLambdaWrapper: kind " << k << " and type " << argType
432
1
                  << "\n";
433
2
  std::vector<api::Term> lvars;
434
2
  std::vector<api::Sort> domainTypes = argType.getFunctionDomainSorts();
435
2
  for (unsigned i = 0, size = domainTypes.size(); i < size; ++i)
436
  {
437
    // the introduced variable is internal (not parsable)
438
2
    std::stringstream ss;
439
1
    ss << "_lvar_" << i;
440
2
    api::Term v = d_solver->mkVar(domainTypes[i], ss.str());
441
1
    lvars.push_back(v);
442
  }
443
  // apply body of lambda to variables
444
  api::Term wrapper =
445
1
      d_solver->mkTerm(api::LAMBDA,
446
2
                       d_solver->mkTerm(api::BOUND_VAR_LIST, lvars),
447
3
                       d_solver->mkTerm(k, lvars));
448
449
2
  return wrapper;
450
}
451
452
1318
api::Term Tptp::getAssertionExpr(FormulaRole fr, api::Term expr)
453
{
454
1318
  switch (fr) {
455
1292
    case FR_AXIOM:
456
    case FR_HYPOTHESIS:
457
    case FR_DEFINITION:
458
    case FR_ASSUMPTION:
459
    case FR_LEMMA:
460
    case FR_THEOREM:
461
    case FR_NEGATED_CONJECTURE:
462
    case FR_PLAIN:
463
      // it's a usual assert
464
1292
      return expr;
465
23
    case FR_CONJECTURE:
466
      // it should be negated when asserted
467
23
      return d_solver->mkTerm(api::NOT, expr);
468
3
    case FR_UNKNOWN:
469
    case FR_FI_DOMAIN:
470
    case FR_FI_FUNCTORS:
471
    case FR_FI_PREDICATES:
472
    case FR_TYPE:
473
      // it does not correspond to an assertion
474
3
      return d_nullExpr;
475
      break;
476
  }
477
  Assert(false);  // unreachable
478
  return d_nullExpr;
479
}
480
481
42
api::Term Tptp::getAssertionDistinctConstants()
482
{
483
84
  std::vector<api::Term> constants;
484
48
  for (std::pair<const std::string, api::Term>& cs : d_distinct_objects)
485
  {
486
6
    constants.push_back(cs.second);
487
  }
488
42
  if (constants.size() > 1)
489
  {
490
3
    return d_solver->mkTerm(api::DISTINCT, constants);
491
  }
492
39
  return d_nullExpr;
493
}
494
495
1318
Command* Tptp::makeAssertCommand(FormulaRole fr,
496
                                 api::Term expr,
497
                                 bool cnf,
498
                                 bool inUnsatCore)
499
{
500
  // For SZS ontology compliance.
501
  // if we're in cnf() though, conjectures don't result in "Theorem" or
502
  // "CounterSatisfiable".
503
1318
  if (!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
504
23
    d_hasConjecture = true;
505
23
    Assert(!expr.isNull());
506
  }
507
1318
  if( expr.isNull() ){
508
3
    return new EmptyCommand("Untreated role for expression");
509
  }else{
510
1315
    return new AssertCommand(expr, inUnsatCore);
511
  }
512
}
513
514
}/* CVC4::parser namespace */
515
26673
}/* CVC4 namespace */