Connect++ 0.7.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 597 of file TPTPParser.hpp.

Member Function Documentation

◆ operator()() [1/7]

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

Definition at line 1369 of file TPTPParser.cpp.

1369 {
1370 FOF result(FOFType::Empty);
1371 FOF lhs = boost::apply_visitor(convert_fof_formula(), f.lhs);
1372 vector<FOF> rhs;
1373 size_t n = f.rhs.size();
1374 for (size_t i = 0; i < n; i++) {
1375 FOF sub = boost::apply_visitor(convert_fof_formula(), f.rhs[i]);
1376 rhs.push_back(sub);
1377 }
1378 rhs.insert(rhs.begin(), lhs);
1379 if (f.type == "&") {
1380 result = FOF(FOFType::And, rhs, nullptr);
1381 return result;
1382 }
1383 if (f.type == "|") {
1384 result = FOF(FOFType::Or, rhs, nullptr);
1385 return result;
1386 }
1387 cerr << "You have an unsupported fof_andor_struct." << endl;
1388 return result;
1389 }
FOF
Representation of first order formulas.
Definition FOF.hpp:58
convert_fof_formula
More complex semantic action for FOF formulas.
Definition TPTPParser.hpp:597

◆ operator()() [2/7]

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

Definition at line 1315 of file TPTPParser.cpp.

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

◆ operator()() [3/7]

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

Definition at line 1279 of file TPTPParser.cpp.

1279 {
1280 FOF sub = boost::apply_visitor(convert_fof_formula(), f.arg);
1281 vector<FOF> subs;
1282 subs.push_back(sub);
1283 FOF result(FOFType::Neg, subs, nullptr);
1284 return result;
1285 }

◆ operator()() [4/7]

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

Definition at line 1234 of file TPTPParser.cpp.

1234 {
1235 size_t arity = f.args.size();
1236 Predicate* new_P =
1237 p_index_p->add_predicate(f.functor, arity);
1238 vector<Term*> args;
1239 for (size_t i = 0; i < arity; i++) {
1240 Term* new_t =
1241 boost::apply_visitor(convert_fof_arguments_struct(),
1242 f.args[i]);
1243 args.push_back(new_t);
1244 }
1245 Literal lit(new_P, args, arity, true);
1246 FOF result(lit);
1247 return result;
1248 }
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:547

◆ operator()() [5/7]

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

Definition at line 1287 of file TPTPParser.cpp.

1287 {
1288 FOF sub = boost::apply_visitor(convert_fof_formula(), f.arg);
1289 size_t n = f.vars.size();
1290 vector<FOF> subs;
1291 subs.push_back(sub);
1292 FOF temp(FOFType::Empty);
1293 if (f.type == "!") {
1294 for (int i = n - 1; i >= 0; i--) {
1295 Variable* var = var_index_p->add_named_var(f.vars[i]);
1296 temp = FOF(FOFType::A, subs, var);
1297 subs.clear();
1298 subs.push_back(temp);
1299 }
1300 return temp;
1301 }
1302 if (f.type == "?") {
1303 for (int i = n - 1; i >= 0; i--) {
1304 Variable* var = var_index_p->add_named_var(f.vars[i]);
1305 temp = FOF(FOFType::E, subs, var);
1306 subs.clear();
1307 subs.push_back(temp);
1308 }
1309 return temp;
1310 }
1311 cerr << "You have an unsupported fof_quantifier_struct." << endl;
1312 return FOF(FOFType::Empty);
1313 }
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:47

◆ operator()() [6/7]

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

Definition at line 1274 of file TPTPParser.cpp.

1274 {
1275 FOF result = boost::apply_visitor(convert_fof_formula(), f.arg);
1276 return result;
1277 }

◆ operator()() [7/7]

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

Definition at line 1250 of file TPTPParser.cpp.

1250 {
1251 size_t arity = 2;
1252 if (!equals_added) {
1253 equals_added = true;
1254 equals_p = p_index_p->add_predicate("=", arity);
1255 }
1256 bool polarity = true;
1257 if (f.connective == "!=")
1258 polarity = false;
1259
1260 vector<Term*> args;
1261 Term* new_t =
1262 boost::apply_visitor(convert_fof_arguments_struct(),
1263 f.left);
1264 args.push_back(new_t);
1265 new_t =
1266 boost::apply_visitor(convert_fof_arguments_struct(),
1267 f.right);
1268 args.push_back(new_t);
1269 Literal lit(equals_p, args, arity, polarity);
1270 FOF result(lit);
1271 return result;
1272 }
The documentation for this struct was generated from the following files: