GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/parser/tptp/tptp.h Lines: 5 7 71.4 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file tptp.h
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
#include "parser/antlr_input.h" // Needs to go first.
18
19
#include "cvc4parser_private.h"
20
21
#ifndef CVC4__PARSER__TPTP_H
22
#define CVC4__PARSER__TPTP_H
23
24
#include <unordered_map>
25
#include <unordered_set>
26
27
#include "api/cvc4cpp.h"
28
#include "parser/parse_op.h"
29
#include "parser/parser.h"
30
#include "util/hash.h"
31
32
namespace CVC4 {
33
34
class Command;
35
36
namespace api {
37
class Solver;
38
}
39
40
namespace parser {
41
42
class Tptp : public Parser {
43
 private:
44
  friend class ParserBuilder;
45
 public:
46
6577
  bool cnf() const { return d_cnf; }
47
1318
  void setCnf(bool cnf) { d_cnf = cnf; }
48
49
152
  bool fof() const { return d_fof; }
50
1318
  void setFof(bool fof) { d_fof = fof; }
51
52
  void forceLogic(const std::string& logic) override;
53
54
  void addFreeVar(api::Term var);
55
  std::vector<api::Term> getFreeVar();
56
57
  api::Term convertRatToUnsorted(api::Term expr);
58
  /**
59
   * Returns a free constant corresponding to the string str. We ensure that
60
   * these constants are one-to-one with str. We assert that all these free
61
   * constants are pairwise distinct before issuing satisfiability queries.
62
   */
63
  api::Term convertStrToUnsorted(std::string str);
64
65
  // CNF and FOF are unsorted so we define this common type.
66
  // This is also the api::Sort of $i in TFF.
67
  api::Sort d_unsorted;
68
69
  enum Theory {
70
    THEORY_CORE,
71
  };/* enum Theory */
72
73
  enum FormulaRole {
74
    FR_AXIOM,
75
    FR_HYPOTHESIS,
76
    FR_DEFINITION,
77
    FR_ASSUMPTION,
78
    FR_LEMMA,
79
    FR_THEOREM,
80
    FR_CONJECTURE,
81
    FR_NEGATED_CONJECTURE,
82
    FR_UNKNOWN,
83
    FR_PLAIN,
84
    FR_FI_DOMAIN,
85
    FR_FI_FUNCTORS,
86
    FR_FI_PREDICATES,
87
    FR_TYPE,
88
  };/* enum FormulaRole */
89
90
42
  bool hasConjecture() const { return d_hasConjecture; }
91
92
 protected:
93
  Tptp(api::Solver* solver,
94
       SymbolManager* sm,
95
       Input* input,
96
       bool strictMode = false,
97
       bool parseOnly = false);
98
99
 public:
100
  ~Tptp();
101
  /**
102
   * Add theory symbols to the parser state.
103
   *
104
   * @param theory the theory to open (e.g., Core, Ints)
105
   */
106
  void addTheory(Theory theory);
107
108
  /** creates a lambda abstraction around application of given kind
109
   *
110
   * Given a kind k and type argType = t1...tn -> t, creates a lambda
111
   * expression
112
   *  (lambda x1:t1,...,xn:tn . (k x1 ... xn)) : t
113
   */
114
  api::Term mkLambdaWrapper(api::Kind k, api::Sort argType);
115
116
  /** get assertion expression, based on the formula role.
117
  * expr should have Boolean type.
118
  * This returns the expression that should be asserted, given the formula role fr.
119
  * For example, if the role is "conjecture", then the return value is the negation of expr.
120
  */
121
  api::Term getAssertionExpr(FormulaRole fr, api::Term expr);
122
123
  /** get assertion for distinct constants
124
   *
125
   * This returns a node of the form distinct( k1, ..., kn ) where k1, ..., kn
126
   * are the distinct constants introduced by this parser (see
127
   * convertStrToUnsorted) if n>1, or null otherwise.
128
   */
129
  api::Term getAssertionDistinctConstants();
130
131
  /** returns the appropriate AssertCommand, given a role, expression expr to
132
   * assert, and information about the assertion. The assertion expr is
133
   * literally what should be asserted (it is already been processed with
134
   * getAssertionExpr above). This may set a flag in the parser to mark
135
   * that we have asserted a conjecture.
136
   */
137
  Command* makeAssertCommand(FormulaRole fr,
138
                             api::Term expr,
139
                             bool cnf,
140
                             bool inUnsatCore);
141
142
  /** Ugly hack because I don't know how to return an expression from a
143
      token */
144
  api::Term d_tmp_expr;
145
146
  /** Push a new stream in the lexer. When EOF is reached the previous stream
147
      is reused */
148
  void includeFile(std::string fileName);
149
150
  /** Check a TPTP let binding for well-formedness. */
151
  void checkLetBinding(const std::vector<api::Term>& bvlist,
152
                       api::Term lhs,
153
                       api::Term rhs,
154
                       bool formula);
155
  /**
156
   * This converts a ParseOp to expression, assuming it is a standalone term.
157
   *
158
   * There are three cases in TPTP: either p already has an expression, in which
159
   * case this function just returns it, or p has just a name or a builtin kind.
160
   */
161
  api::Term parseOpToExpr(ParseOp& p);
162
  /**
163
   * Apply parse operator to list of arguments, and return the resulting
164
   * expression.
165
   *
166
   * args must not be empty (otherwise the above method should have been
167
   * called).
168
   *
169
   * There are three cases in TPTP: either p already has an expression, in which
170
   * case this function just applies it to the arguments, or p has
171
   * just a name or a builtin kind, in which case the respective operator is
172
   * built.
173
   *
174
   * Note that the case of uninterpreted functions in TPTP this need not have
175
   * been previously declared, which leads to a more convoluted processing than
176
   * what is necessary in parsing SMT-LIB.
177
   */
178
  api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args);
179
180
 private:
181
  void addArithmeticOperators();
182
183
  // In CNF variable are implicitly binded
184
  // d_freevar collect them
185
  std::vector<api::Term> d_freeVar;
186
  api::Term d_rtu_op;
187
  api::Term d_stu_op;
188
  api::Term d_utr_op;
189
  api::Term d_uts_op;
190
  // The set of expression that already have a bridge
191
  std::unordered_set<api::Term, api::TermHashFunction> d_r_converted;
192
  std::unordered_map<std::string, api::Term> d_distinct_objects;
193
194
  std::vector< pANTLR3_INPUT_STREAM > d_in_created;
195
196
  // TPTP directory where to find includes;
197
  // empty if none could be determined
198
  std::string d_tptpDir;
199
200
  // the null expression
201
  api::Term d_nullExpr;
202
203
  // hack to make output SZS ontology-compliant
204
  bool d_hasConjecture;
205
206
  bool d_cnf; // in a cnf formula
207
  bool d_fof; // in an fof formula
208
};/* class Tptp */
209
210
211
namespace tptp {
212
/**
213
 * Just exists to provide the uintptr_t constructor that ANTLR
214
 * requires.
215
 */
216
struct myExpr : public CVC4::api::Term
217
{
218
  myExpr() : CVC4::api::Term() {}
219
  myExpr(void*) : CVC4::api::Term() {}
220
  myExpr(const CVC4::api::Term& e) : CVC4::api::Term(e) {}
221
  myExpr(const myExpr& e) : CVC4::api::Term(e) {}
222
}; /* struct myExpr*/
223
224
enum NonAssoc {
225
  NA_IFF,
226
  NA_IMPLIES,
227
  NA_REVIMPLIES,
228
  NA_REVIFF,
229
  NA_REVOR,
230
  NA_REVAND,
231
};
232
233
}/* CVC4::parser::tptp namespace */
234
235
236
}/* CVC4::parser namespace */
237
}/* CVC4 namespace */
238
239
#endif /* CVC4__PARSER__TPTP_INPUT_H */