Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | List of all members
convert_fof_formula Struct Reference

More complex semantic action for FOF formulas. More...

#include <TPTPParser.hpp>

Inheritance diagram for convert_fof_formula:
Inheritance graph
[legend]
Collaboration diagram for convert_fof_formula:
Collaboration graph
[legend]

Public Member Functions

FOF operator() (const fof_plain_term_struct &) const
 
FOF operator() (const infix_struct &) const
 
FOF operator() (const fof_unitary_formula_struct &) const
 
FOF operator() (const fof_negation_struct &) const
 
FOF operator() (const fof_quantifier_struct &) const
 
FOF operator() (const fof_binary_struct &) const
 
FOF operator() (const fof_andor_struct &) const
 

Detailed Description

More complex semantic action for FOF formulas.

Functions etc to make a FOF formula.

Definition at line 594 of file TPTPParser.hpp.

Member Function Documentation

◆ operator()() [1/7]

FOF convert_fof_formula::operator() ( const fof_andor_struct & f) const

Definition at line 1358 of file TPTPParser.cpp.

1358 {
1359 FOF result(FOFType::Empty);
1360 FOF lhs = boost::apply_visitor(convert_fof_formula(), f.lhs);
1361 vector<FOF> rhs;
1362 size_t n = f.rhs.size();
1363 for (size_t i = 0; i < n; i++) {
1364 FOF sub = boost::apply_visitor(convert_fof_formula(), f.rhs[i]);
1365 rhs.push_back(sub);
1366 }
1367 rhs.insert(rhs.begin(), lhs);
1368 if (f.type == "&") {
1369 result = FOF(FOFType::And, rhs, nullptr);
1370 return result;
1371 }
1372 if (f.type == "|") {
1373 result = FOF(FOFType::Or, rhs, nullptr);
1374 return result;
1375 }
1376 cerr << "You have an unsupported fof_andor_struct." << endl;
1377 return result;
1378 }
FOF
Representation of first order formulas.
Definition FOF.hpp:57
convert_fof_formula
More complex semantic action for FOF formulas.
Definition TPTPParser.hpp:594

◆ operator()() [2/7]

FOF convert_fof_formula::operator() ( const fof_binary_struct & f) const

Definition at line 1304 of file TPTPParser.cpp.

1304 {
1305 FOF lhs = boost::apply_visitor(convert_fof_formula(), f.lhs);
1306 FOF rhs = boost::apply_visitor(convert_fof_formula(), f.rhs);
1307 vector<FOF> subs;
1308 FOF result(FOFType::Empty);
1309 if (f.type == "<=") {
1310 subs.push_back(rhs);
1311 subs.push_back(lhs);
1312 result = FOF(FOFType::Imp, subs, nullptr);
1313 return result;
1314 }
1315 subs.push_back(lhs);
1316 subs.push_back(rhs);
1317 if (f.type == "=>") {
1318 result = FOF(FOFType::Imp, subs, nullptr);
1319 return result;
1320 }
1321 if (f.type == "<=>") {
1322 result = FOF(FOFType::Iff, subs, nullptr);
1323 return result;
1324 }
1325 if (f.type == "<~>") {
1326 FOF not_lhs = lhs;
1327 not_lhs.negate();
1328 FOF not_rhs = rhs;
1329 not_rhs.negate();
1330 vector<FOF> new_subs_1;
1331 new_subs_1.push_back(lhs);
1332 new_subs_1.push_back(not_rhs);
1333 vector<FOF> new_subs_2;
1334 new_subs_2.push_back(not_lhs);
1335 new_subs_2.push_back(rhs);
1336 FOF new_lhs(FOFType::And, new_subs_1, nullptr);
1337 FOF new_rhs(FOFType::And, new_subs_2, nullptr);
1338 subs.clear();
1339 subs.push_back(new_lhs);
1340 subs.push_back(new_rhs);
1341 result = FOF(FOFType::Or, subs, nullptr);
1342 return result;
1343 }
1344 if (f.type == "~|") {
1345 result = FOF(FOFType::Or, subs, nullptr);
1346 result.negate();
1347 return result;
1348 }
1349 if (f.type == "~&") {
1350 result = FOF(FOFType::And, subs, nullptr);
1351 result.negate();
1352 return result;
1353 }
1354 cerr << "You have an unsupported fof_binary_struct." << endl;
1355 return result;
1356 }
FOF::negate
void negate()
Negate an FOF, applying obvious simplifications if it's already negated or an implication.
Definition FOF.cpp:398

◆ operator()() [3/7]

FOF convert_fof_formula::operator() ( const fof_negation_struct & f) const

Definition at line 1268 of file TPTPParser.cpp.

1268 {
1269 FOF sub = boost::apply_visitor(convert_fof_formula(), f.arg);
1270 vector<FOF> subs;
1271 subs.push_back(sub);
1272 FOF result(FOFType::Neg, subs, nullptr);
1273 return result;
1274 }

◆ operator()() [4/7]

FOF convert_fof_formula::operator() ( const fof_plain_term_struct & f) const

Definition at line 1223 of file TPTPParser.cpp.

1223 {
1224 size_t arity = f.args.size();
1225 Predicate* new_P =
1226 p_index_p->add_predicate(f.functor, arity);
1227 vector<Term*> args;
1228 for (size_t i = 0; i < arity; i++) {
1229 Term* new_t =
1230 boost::apply_visitor(convert_fof_arguments_struct(),
1231 f.args[i]);
1232 args.push_back(new_t);
1233 }
1234 Literal lit(new_P, args, arity, true);
1235 FOF result(lit);
1236 return result;
1237 }
Literal
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
Predicate
Basic representation of predicates: here just names, ids and arities.
Definition Predicate.hpp:51
PredicateIndex::add_predicate
Predicate * add_predicate(const string &, Arity)
Self-explanatory.
Definition PredicateIndex.cpp:40
Term
General representation of terms.
Definition Term.hpp:62
convert_fof_arguments_struct
More complex semantic actions, now functions etc to make a literal.
Definition TPTPParser.hpp:544

◆ operator()() [5/7]

FOF convert_fof_formula::operator() ( const fof_quantifier_struct & f) const

Definition at line 1276 of file TPTPParser.cpp.

1276 {
1277 FOF sub = boost::apply_visitor(convert_fof_formula(), f.arg);
1278 size_t n = f.vars.size();
1279 vector<FOF> subs;
1280 subs.push_back(sub);
1281 FOF temp(FOFType::Empty);
1282 if (f.type == "!") {
1283 for (int i = n - 1; i >= 0; i--) {
1284 Variable* var = var_index_p->add_named_var(f.vars[i]);
1285 temp = FOF(FOFType::A, subs, var);
1286 subs.clear();
1287 subs.push_back(temp);
1288 }
1289 return temp;
1290 }
1291 if (f.type == "?") {
1292 for (int i = n - 1; i >= 0; i--) {
1293 Variable* var = var_index_p->add_named_var(f.vars[i]);
1294 temp = FOF(FOFType::E, subs, var);
1295 subs.clear();
1296 subs.push_back(temp);
1297 }
1298 return temp;
1299 }
1300 cerr << "You have an unsupported fof_quantifier_struct." << endl;
1301 return FOF(FOFType::Empty);
1302 }
Variable
Basic representation of variables.
Definition Variable.hpp:58
VariableIndex::add_named_var
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.
Definition VariableIndex.cpp:44

◆ operator()() [6/7]

FOF convert_fof_formula::operator() ( const fof_unitary_formula_struct & f) const

Definition at line 1263 of file TPTPParser.cpp.

1263 {
1264 FOF result = boost::apply_visitor(convert_fof_formula(), f.arg);
1265 return result;
1266 }

◆ operator()() [7/7]

FOF convert_fof_formula::operator() ( const infix_struct & f) const

Definition at line 1239 of file TPTPParser.cpp.

1239 {
1240 size_t arity = 2;
1241 if (!equals_added) {
1242 equals_added = true;
1243 equals_p = p_index_p->add_predicate("=", arity);
1244 }
1245 bool polarity = true;
1246 if (f.connective == "!=")
1247 polarity = false;
1248
1249 vector<Term*> args;
1250 Term* new_t =
1251 boost::apply_visitor(convert_fof_arguments_struct(),
1252 f.left);
1253 args.push_back(new_t);
1254 new_t =
1255 boost::apply_visitor(convert_fof_arguments_struct(),
1256 f.right);
1257 args.push_back(new_t);
1258 Literal lit(equals_p, args, arity, polarity);
1259 FOF result(lit);
1260 return result;
1261 }
The documentation for this struct was generated from the following files: