Connect++ 0.3.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | List of all members
TPTPParser Class Reference

Wrap up everything the TPTP parser needs to do inside a single class. More...

#include <TPTPParser.hpp>

Collaboration diagram for TPTPParser:
Collaboration graph
[legend]

Public Member Functions

 TPTPParser ()=delete
 You definitely don't want this constructor.
 
 TPTPParser (VariableIndex *, FunctionIndex *, TermIndex *, PredicateIndex *, Matrix *)
 The only constructor that makes sense.
 
bool parse_tptp_from_file (const string &)
 Main method to parse from a TPTP file to the data structures needed by the prover.
 
void show_file_includes ()
 Show any includes present in the TPTP file.
 
void clear ()
 Clear everything associated with the TPTP parser.
 
vector< string > get_defined_items ()
 Get a copy of tptp_parser::all_defined.
 
vector< string > get_system_items ()
 Get a copy of tptp_parser::all_system.
 
bool equality_used ()
 Did equality turn up anywhere in the parse?
 
bool conjecture_present () const
 Did a conjecture turn up anywhere in the parse?
 
bool negated_conjecture_present () const
 Did a negated conjecture turn up anywhere in the parse?
 
bool no_conjecture_clause () const
 When you analysed the original problem, did you conclude that it has no conjecture clauses that can be used as a starting point?
 
size_t number_of_fof_formulas () const
 How many first-order formulas turned up in the parse?
 
string get_problem_status ()
 The parse tries to identify the problem status.
 
Predicateget_equals_predicate () const
 If equality turned up anywhere in the parse it will have been turned into an actual Predicate, so this will give you a pointer to it.
 
bool problem_is_cnf_only () const
 Self-explanatory.
 
bool fof_conjecture_is_true () const
 Self-explanatory.
 
bool fof_conjecture_is_false () const
 Self-explanatory.
 
bool fof_conjecture_is_missing () const
 Was there a conjecture clause in the problem file?
 
bool fof_negated_conjecture_removed () const
 Was there a conjecture clause that got simplified away?
 
bool simplified_fof_has_axioms () const
 Where there any axioms for an FOF problem after simplification?
 
bool fof_has_axioms () const
 Where there any axioms for an FOF problem before simplification?
 

Private Member Functions

void read_tptp_from_file (const string &)
 Read the file into a string, while stripping out and collecting comment blocks.
 

Private Attributes

string file_contents
 Contents of the TPTP file, with comments removed.
 
vector< string > comment_blocks
 Each comment is stored here.
 
VariableIndexvip
 The class has pointers to all the relevant indices.
 
FunctionIndexfip
 The class has pointers to all the relevant indices.
 
TermIndextip
 The class has pointers to all the relevant indices.
 
PredicateIndexpip
 The class has pointers to all the relevant indices.
 
Matrixmatrix
 The class has a pointer to the matrix, and can therefore construct it as it parses.
 

Detailed Description

Wrap up everything the TPTP parser needs to do inside a single class.

This class needs access to the assorted indices employed by the prover because they are the only things anyone should be using to make Terms, Variables etc.

If you construct this properly and use parse_tptp_from_file, then after a successful parse the indices have everything ready to go.

Definition at line 658 of file TPTPParser.hpp.

Constructor & Destructor Documentation

◆ TPTPParser()

TPTPParser::TPTPParser ( VariableIndex new_vip,
FunctionIndex new_fip,
TermIndex new_tip,
PredicateIndex new_pip,
Matrix new_matrix 
)

The only constructor that makes sense.

Definition at line 1406 of file TPTPParser.cpp.

1413:
1416vip(new_vip),
1417fip(new_fip),
1418tip(new_tip),
1419pip(new_pip),
1420matrix(new_matrix) {
1421 // var_index_p is global in the tptp_parser namespace. It is
1422 // used by semantic actions.
1423 var_index_p = new_vip;
1424 // Similar for fun_index_p and so on...
1425 fun_index_p = new_fip;
1426 t_index_p = new_tip;
1427 p_index_p = new_pip;
1428 // And remember that FOF also needs to use the indices.
1429 FOF::set_indexes(std::tuple<VariableIndex*, FunctionIndex*, PredicateIndex*, TermIndex*>
1430 (new_vip, new_fip, new_pip, new_tip));
1431 clear();
1432};
static void set_indexes(std::tuple< VariableIndex *, FunctionIndex *, PredicateIndex *, TermIndex * > is)
Set up pointer to the variable index etc.
Definition FOF.hpp:236
void clear()
Clear everything associated with the TPTP parser.
vector< string > comment_blocks
Each comment is stored here.
TermIndex * tip
The class has pointers to all the relevant indices.
FunctionIndex * fip
The class has pointers to all the relevant indices.
PredicateIndex * pip
The class has pointers to all the relevant indices.
Matrix * matrix
The class has a pointer to the matrix, and can therefore construct it as it parses.
string file_contents
Contents of the TPTP file, with comments removed.
VariableIndex * vip
The class has pointers to all the relevant indices.

Member Function Documentation

◆ clear()

void TPTPParser::clear ( )

Clear everything associated with the TPTP parser.

Note that this is slightly messy because it also clears all the supporting stuff that's global in the tptp_parser namespace. Yes, very ugly. What ya gonna do about it!!??

Definition at line 1896 of file TPTPParser.cpp.

1896 {
1897 equals_added = false;
1898 conjecture_found = false;
1899 negated_conjecture_found = false;
1900 conjecture_true = false;
1901 conjecture_false = false;
1902 found_true_axiom = false;
1903 found_false_axiom = false;
1904 negated_conjecture_exists = false;
1905 has_axioms = false;
1906 has_axioms_remaining = false;
1907 cnf_only = false;
1908 number_of_negated_conjecture_clauses = 0;
1909 number_of_simplified_negated_conjecture_clauses = 0;
1910 equals_p = nullptr;
1911 neg_lit = false;
1912 is_first_status = true;
1913 current_clause_role = "";
1914 current_formula_role = "";
1915 current_formula_name = "";
1916 clause_roles.clear();
1917 formula_roles.clear();
1918 formula_names.clear();
1919 file_contents.clear();
1920 comment_blocks.clear();
1921 status = "";
1922 all_defined.clear();
1923 all_system.clear();
1924 distinct_objects.clear();
1925 current_clause.clear();
1926 current_formula.clear();
1927 all_formulas.clear();
1928 all_clauses.clear();
1929 file_includes.clear();
1930 to_include.clear();
1931 include_this_item = true;
1932 include_file_path = fs::path();
1933}
void clear()
Straightforward reset method.
Definition Clause.hpp:86
void clear()
Make an FOFType::Empty.
Definition FOF.hpp:265

◆ conjecture_present()

bool TPTPParser::conjecture_present ( ) const

Did a conjecture turn up anywhere in the parse?

Definition at line 2096 of file TPTPParser.cpp.

2096 {
2097 return conjecture_found;
2098}

◆ equality_used()

bool TPTPParser::equality_used ( )

Did equality turn up anywhere in the parse?

Definition at line 1943 of file TPTPParser.cpp.

1943 {
1944 return equals_added;
1945}

◆ fof_conjecture_is_false()

bool TPTPParser::fof_conjecture_is_false ( ) const

Self-explanatory.

Definition at line 2119 of file TPTPParser.cpp.

2119 {
2120 return conjecture_false;
2121}

◆ fof_conjecture_is_missing()

bool TPTPParser::fof_conjecture_is_missing ( ) const

Was there a conjecture clause in the problem file?

Definition at line 2123 of file TPTPParser.cpp.

2123 {
2124 return !conjecture_found;
2125}

◆ fof_conjecture_is_true()

bool TPTPParser::fof_conjecture_is_true ( ) const

Self-explanatory.

Definition at line 2114 of file TPTPParser.cpp.

2114 {
2115 return conjecture_true;
2116}

◆ fof_has_axioms()

bool TPTPParser::fof_has_axioms ( ) const

Where there any axioms for an FOF problem before simplification?

Definition at line 2135 of file TPTPParser.cpp.

2135 {
2136 return has_axioms;
2137}

◆ fof_negated_conjecture_removed()

bool TPTPParser::fof_negated_conjecture_removed ( ) const

Was there a conjecture clause that got simplified away?

Definition at line 2127 of file TPTPParser.cpp.

2127 {
2128 return conjecture_found && (number_of_simplified_negated_conjecture_clauses == 0);
2129}

◆ get_defined_items()

vector< string > TPTPParser::get_defined_items ( )

Get a copy of tptp_parser::all_defined.

These are gathered during the parse and may be useful.

Definition at line 1935 of file TPTPParser.cpp.

1935 {
1936 return all_defined;
1937}

◆ get_equals_predicate()

Predicate * TPTPParser::get_equals_predicate ( ) const

If equality turned up anywhere in the parse it will have been turned into an actual Predicate, so this will give you a pointer to it.

Definition at line 1955 of file TPTPParser.cpp.

1955 {
1956 if (equals_added)
1957 return equals_p;
1958 else
1959 return nullptr;
1960}

◆ get_problem_status()

string TPTPParser::get_problem_status ( )

The parse tries to identify the problem status.

Definition at line 1951 of file TPTPParser.cpp.

1951 {
1952 return status;
1953}

◆ get_system_items()

vector< string > TPTPParser::get_system_items ( )

Get a copy of tptp_parser::all_system.

These are gathered during the parse and may be useful.

Definition at line 1939 of file TPTPParser.cpp.

1939 {
1940 return all_system;
1941}

◆ negated_conjecture_present()

bool TPTPParser::negated_conjecture_present ( ) const

Did a negated conjecture turn up anywhere in the parse?

Definition at line 2100 of file TPTPParser.cpp.

2100 {
2101 return negated_conjecture_found;
2102}

◆ no_conjecture_clause()

bool TPTPParser::no_conjecture_clause ( ) const

When you analysed the original problem, did you conclude that it has no conjecture clauses that can be used as a starting point?

Definition at line 2104 of file TPTPParser.cpp.

2104 {
2105 return ((all_formulas.size() > 0 && !conjecture_found) ||
2106 (all_formulas.size() > 0 && (conjecture_true || conjecture_false)) ||
2107 (all_formulas.size() == 0 && !negated_conjecture_found) ||
2108 (all_formulas.size() == 0 && !negated_conjecture_exists));
2109}

◆ number_of_fof_formulas()

size_t TPTPParser::number_of_fof_formulas ( ) const

How many first-order formulas turned up in the parse?

Definition at line 1947 of file TPTPParser.cpp.

1947 {
1948 return all_formulas.size();
1949}

◆ parse_tptp_from_file()

bool TPTPParser::parse_tptp_from_file ( const string &  file_name)

Main method to parse from a TPTP file to the data structures needed by the prover.

This first uses read_tptp_from_file to strip out comments. It then uses TPTP_file_grammar with qi::phrase_parse to parse the file.

As a side effect of that, a bunch of things such as all_clauses and clause_roles, which are global in the tptp_parser namespace, get set up. These are then used to populate the matrix etc.

Parameters
file_nameReference to string containing the file name.

Definition at line 1478 of file TPTPParser.cpp.

1478 {
1479 /*
1480 * Let the parser do the heavy-lifting: get stuff from the
1481 * TPTP file and parse it.
1482 */
1483 read_tptp_from_file(file_name);
1484
1485 Iter start = file_contents.begin();
1486 Iter end = file_contents.end();
1487
1488 include_file_path = params::full_problem_path;
1489
1490 TPTP_file_grammar<Iter> g;
1491 bool result = qi::phrase_parse(start, end, g, ascii::space);
1492
1493 if (start != end || !result)
1494 throw (file_parse_exception(file_name));
1495 /*
1496 * If you get to here, then the parser has read everything and set
1497 * up a whole bunch of stuff for you. In particular, all_clauses and
1498 * all_formulas have the juicy stuff.
1499 *
1500 * However, what follows gets stupidly complicated because you
1501 * have to deal with a lot of rare special cases. :-(
1502 */
1503 if (pip->true_false_added() && params::verbosity > 1)
1504 cout << "Found true/false." << endl;
1505 /*
1506 * First, deal with cnf(...). entries. There's not much to
1507 * do as simplification can happen later.
1508 */
1509 if (negated_conjecture_found && params::verbosity > 1)
1510 cout << "Found negated conjecture." << endl;
1511 /*
1512 * Now do clause conversion for the fof(...). entries.
1513 *
1514 * Remember: negate the conjecture if necessary.
1515 */
1516 if (conjecture_found && params::verbosity > 1)
1517 cout << "Found conjecture." << endl;
1518 /*
1519 * Were there and first_order items, or is it just CNF?
1520 */
1521 cnf_only = (all_formulas.size() == 0);
1522 if (cnf_only && params::verbosity > 1)
1523 cout << "The problem is CNF only." << endl;
1524 /*
1525 * First do a check for general oddness.
1526 */
1527 if (negated_conjecture_found && conjecture_found) {
1528 cout << "% SZS status Error for "
1529 << params::problem_name
1530 << " : conjecture and negated conjecture found in the same problem." << endl;
1531 exit(EXIT_FAILURE);
1532 }
1533 if (!negated_conjecture_found && !conjecture_found && params::verbosity > 1) {
1534 cout << "No conjecture or negated conjecture found." << endl;
1535 }
1536 if (negated_conjecture_found && all_formulas.size() > 0 && params::verbosity > 1) {
1537 cout << "% SZS status Error for "
1538 << params::problem_name
1539 << " : negated conjecture found in FOF problem." << endl;
1540 exit(EXIT_FAILURE);
1541 }
1542 /*
1543 * Now we can convert some formulas to clauses.
1544 *
1545 * Remember: different things need to happen here depending on the state
1546 * of params::no_definitional and params::all_definitional.
1547 */
1548 if (params::no_definitional && params::all_definitional) {
1549 cout << "% SZS status Error for "
1550 << params::problem_name
1551 << " : --all-definitional and --no-definitional have both been set." << endl;
1552 exit(EXIT_FAILURE);
1553 }
1554 /*
1555 * Later on I'll need to know whether the original (FOF) problem
1556 * actually had axioms.
1557 */
1558 has_axioms = (all_clauses.size() > 0);
1559 if (!has_axioms) {
1560 for (const string& s : formula_roles) {
1561 if (s != "conjecture") {
1562 has_axioms = true;
1563 break;
1564 }
1565 }
1566 }
1567 /*
1568 * Do the conversion to clauses and store the results.
1569 * Don't simplify yet.
1570 */
1571 vector<vector<Clause>> all_fof_clauses;
1572 bool found_one_conjecture = false;
1573 vector<bool> definitional_conversion;
1574 size_t i = 0;
1575 size_t conjecture_index = 0;
1576 for (FOF f : all_formulas) {
1577 vector<Clause> vc;
1578 if (formula_roles[i] == string("conjecture")) {
1579 conjecture_index = i;
1580 if (found_one_conjecture) {
1581 cout << "% SZS status Error for "
1582 << params::problem_name
1583 << " : more than one conjecture in the input file." << endl;
1584 exit(EXIT_FAILURE);
1585 }
1586 else {
1587 found_one_conjecture = true;
1588 }
1589 // This is rather important!
1590 f.negate();
1591 if (!params::no_definitional) {
1592 f.definitional_convert_to_cnf_clauses(vc);
1593 definitional_conversion.push_back(true);
1594 }
1595 else {
1596 f.convert_to_cnf_clauses(vc);
1597 definitional_conversion.push_back(false);
1598 }
1599 number_of_negated_conjecture_clauses = vc.size();
1600 }
1601 else {
1602 if (params::all_definitional || !conjecture_found) {
1603 f.definitional_convert_to_cnf_clauses(vc);
1604 definitional_conversion.push_back(true);
1605 }
1606 else {
1607 f.convert_to_cnf_clauses(vc);
1608 definitional_conversion.push_back(false);
1609 }
1610 }
1611 all_fof_clauses.push_back(vc);
1612 i++;
1613 }
1614 /*
1615 * Now all_fof_clauses has unsimplified clauses, as
1616 * does all_clauses. We also know where any conjecture
1617 * is.
1618 *
1619 * Before doing anything else, it might be that all we
1620 * want is to see the clause conversion.
1621 */
1622 i = 0;
1623 if (params::show_clauses) {
1624 for (vector<Clause>& vc : all_fof_clauses) {
1625 cout << "---------------------" << endl;
1626 cout << "Formula: " << formula_names[i] << ", "
1627 << formula_roles[i] << endl;
1628 cout << all_formulas[i] << endl;
1629 cout << "Clauses:";
1630 if (definitional_conversion[i]) {
1631 cout << " (definitional conversion)";
1632 }
1633 cout << endl;
1635 for (const Clause& c : vc) {
1636 cout << c << endl;
1637 }
1638 i++;
1639 }
1640 exit(EXIT_SUCCESS);
1641 }
1642 /*
1643 * OK - so we've got more to do. Now simplify everything,
1644 * but keep track of any strange cases.
1645 *
1646 * Start with the case when the problem is CNF only.
1647 */
1648 SimplificationResult cnf_result = FOF::simplify_cnf(all_clauses, clause_roles);
1649 /*
1650 * Did we somehow manage to delete all the negated conjectures?
1651 */
1652 for (const string& s : clause_roles) {
1653 if (s == string("negated_conjecture")) {
1654 negated_conjecture_exists = true;
1655 break;
1656 }
1657 }
1658 string output_string;
1659 vector<Clause> simplified_fof_clauses;
1660 vector<string> simplified_fof_roles;
1661 /*
1662 * Note that we can draw the following conclusions regardless of whether
1663 * or not any equality axioms have been added.
1664 */
1665 if (all_formulas.size() == 0) {
1666 if (cnf_result == SimplificationResult::Tautology) {
1667 output_string = "Satisfiable";
1668 }
1669 if (cnf_result == SimplificationResult::Contradiction) {
1670 output_string = "Unsatisfiable";
1671 }
1672 if (output_string != "") {
1673 cout << "% SZS status " << output_string << " for "
1674 << params::problem_name
1675 << " : established by clause simplification." << endl;
1676 std::exit(EXIT_SUCCESS);
1677 }
1678 }
1679 // Here, we know it's a problem with FOF stuff in it.
1680 else {
1681 i = 0;
1682 for (vector<Clause> cs : all_fof_clauses) {
1683 SimplificationResult fof_result = FOF::simplify_cnf(cs);
1684
1685 if (i == conjecture_index && conjecture_found) {
1686 number_of_simplified_negated_conjecture_clauses = cs.size();
1687 }
1688
1689 if (params::generate_tptp_proof) {
1690 params::tptp_conversion_string += "\n% Formula: ";
1691 params::tptp_conversion_string += formula_names[i];
1692 params::tptp_conversion_string += " ( ";
1693 params::tptp_conversion_string += formula_roles[i];
1694 params::tptp_conversion_string += " ) ";
1695 if (definitional_conversion[i]) {
1696 params::tptp_conversion_string += "(definitionally) ";
1697 }
1698 params::tptp_conversion_string += "converted to clauses:\n";
1699 }
1700
1701 if (fof_result == SimplificationResult::Tautology) {
1702 if (i == conjecture_index && conjecture_found) {
1703 conjecture_false = true;
1704 if (params::verbosity > 1) {
1705 cout << "The conjecture is equivalent to $false." << endl;
1706 }
1707 }
1708 else {
1709 found_true_axiom = true;
1710 if (params::verbosity > 1) {
1711 cout << "Axiom is equivalent to $true." << endl;
1712 }
1713 }
1714 if (params::generate_tptp_proof) {
1715 params::tptp_conversion_string += "cnf(";
1716 params::tptp_conversion_string += string(formula_names[i]);
1717 params::tptp_conversion_string += ", ";
1718 if (formula_roles[i] == string("conjecture"))
1719 params::tptp_conversion_string += "negated_conjecture";
1720 else
1721 params::tptp_conversion_string += formula_roles[i];
1722 params::tptp_conversion_string += ", $true).\n";
1723 }
1724 i++;
1725 continue;
1726 }
1727 else if (fof_result == SimplificationResult::Contradiction) {
1728 if (i == conjecture_index && conjecture_found) {
1729 conjecture_true = true;
1730 if (params::verbosity > 1) {
1731 cout << "The conjecture is equivalent to $true." << endl;
1732 }
1733 }
1734 else {
1735 found_false_axiom = true;
1736 if (params::verbosity > 1) {
1737 cout << "Axiom is equivalent to $false." << endl;
1738 }
1739 }
1740 if (params::generate_tptp_proof) {
1741 params::tptp_conversion_string += "cnf(";
1742 params::tptp_conversion_string += string(formula_names[i]);
1743 params::tptp_conversion_string += ", ";
1744 if (formula_roles[i] == string("conjecture"))
1745 params::tptp_conversion_string += "negated_conjecture";
1746 else
1747 params::tptp_conversion_string += formula_roles[i];
1748 params::tptp_conversion_string += ", $false).\n";
1749 }
1750 i++;
1751 continue;
1752 }
1753 else {
1754 size_t clause_count = 1;
1755 for (const Clause& c : cs) {
1756 simplified_fof_clauses.push_back(c);
1757 simplified_fof_roles.push_back(formula_roles[i]);
1758 if (params::generate_tptp_proof) {
1759 params::tptp_conversion_string += "cnf(";
1760 params::tptp_conversion_string += string(formula_names[i]);
1761 params::tptp_conversion_string += "-";
1762 params::tptp_conversion_string += std::to_string(clause_count);
1763 params::tptp_conversion_string += ", ";
1764 if (formula_roles[i] == string("conjecture"))
1765 params::tptp_conversion_string += "negated_conjecture";
1766 else
1767 params::tptp_conversion_string += formula_roles[i];
1768 params::tptp_conversion_string += ", ";
1769 params::tptp_conversion_string += c.to_tptp_string();
1770 params::tptp_conversion_string += ").";
1771 params::tptp_conversion_string += "\n";
1772 }
1773 clause_count++;
1774 }
1775 i++;
1776 }
1777 }
1778 }
1779 /*
1780 * Remember: this actually does some setup work, so don't do it
1781 * until *everything* else is in place. In particular, definitional
1782 * clause conversion can introduce new predicates, so this has to
1783 * happen later.
1784 */
1786
1787 i = 0;
1788 for (Clause& c : all_clauses)
1789 matrix->add_clause(c, clause_roles[i++]);
1790 /*
1791 * If it's a CNF only problem we're done! However, if there are FOF
1792 * clauses then we have to deal with all the silly possibilities.
1793 */
1794 if (all_formulas.size() > 0) {
1795 /*
1796 * Now I know about all odd instances where a part of the problem
1797 * gave rise to clauses that were equivalent to $true or $false.
1798 *
1799 * Does this allow me to stop?
1800 */
1801 string output_string;
1802 if (cnf_result == SimplificationResult::Contradiction || found_false_axiom) {
1803 if (conjecture_true) {
1804 output_string = "TautologousConclusionContradictoryAxioms";
1805 }
1806 else if (conjecture_false) {
1807 output_string = "UnsatisfiableConclusionContradictoryAxioms";
1808 }
1809 else if (!conjecture_found) {
1810 output_string = "Unsatisfiable";
1811 }
1812 else {
1813 output_string = "ContradictoryAxioms";
1814 }
1815 }
1816 else {
1817 /*
1818 * The case of something in the axioms being $true just shrinks the
1819 * set of axioms. So you need to handle the situation where there
1820 * are no axioms remaining!
1821 */
1822 has_axioms_remaining = (all_clauses.size() > 0);
1823 if (!has_axioms_remaining) {
1824 for (const string& s : simplified_fof_roles) {
1825 if (s != "conjecture") {
1826 has_axioms_remaining = true;
1827 break;
1828 }
1829 }
1830 }
1831 if (has_axioms_remaining) {
1832 /*
1833 * So: assuming you have some axioms, what happens if the conjecture
1834 * was $true or $false?
1835 *
1836 * If the conjecture is $false then, as you have axioms, the outcome
1837 * still needs to be determined in case the axioms are contradictory.
1838 */
1839 if (conjecture_true) {
1840 output_string = "Theorem";
1841 }
1842 /*
1843 * We now have just axioms, or axioms with a false conjecture, so
1844 * keep going and sort it out later --
1845 */
1846 }
1847 /*
1848 * We have no axioms.
1849 */
1850 else {
1851 if (conjecture_true) {
1852 output_string = "Theorem";
1853 }
1854 if (conjecture_false) {
1855 output_string = "CounterSatisfiable";
1856 }
1857 if (!conjecture_found) {
1858 output_string = "Theorem";
1859 }
1860 /*
1861 * We now have just a conjecture (or not), so keep going and sort it out
1862 * later --
1863 */
1864 }
1865 }
1866 if (output_string != "") {
1867 cout << "% SZS status " << output_string << " for "
1868 << params::problem_name
1869 << " : established by clause simplification." << endl;
1870 exit(EXIT_SUCCESS);
1871 }
1872 /*
1873 * If none of the special cases forced us to stop, then add the
1874 * FOF material to the matrix.
1875 */
1876 i = 0;
1877 for (Clause& c : simplified_fof_clauses) {
1878 matrix->add_clause(c, simplified_fof_roles[i++]);
1879 }
1880 }
1881 return true;
1882}
Representation of clauses.
Definition Clause.hpp:52
Representation of first order formulas.
Definition FOF.hpp:57
static SimplificationResult simplify_cnf(vector< Clause > &)
Simplify the clauses in a CNF using the method in Clause.
Definition FOF.cpp:1268
void add_clause(Clause &, string="")
Add a Clause to the Matrix and update the index accordingly.
Definition Matrix.cpp:91
void set_num_preds(size_t)
Make an empty index.
Definition Matrix.cpp:42
bool true_false_added() const
Sometimes $true and $false appear in the TPTP collection. See if you included them during the parsing...
size_t get_num_preds() const
Basic get method.
void read_tptp_from_file(const string &)
Read the file into a string, while stripping out and collecting comment blocks.
Exception used by the application in main(...).

◆ problem_is_cnf_only()

bool TPTPParser::problem_is_cnf_only ( ) const

Self-explanatory.

Definition at line 2110 of file TPTPParser.cpp.

2110 {
2111 return cnf_only;
2112}

◆ read_tptp_from_file()

void TPTPParser::read_tptp_from_file ( const string &  file_name)
private

Read the file into a string, while stripping out and collecting comment blocks.

(Yes, better done with a custom skip parser, but writing those is a pain.)

Parameters
file_nameReference to a string containing the file name

Definition at line 1434 of file TPTPParser.cpp.

1434 {
1435 // Used to collect up comments as you see them.
1436 string comment;
1437 bool in_comment = false;
1438
1439 char c;
1440
1441 ifstream file;
1442 file.unsetf(std::ios_base::skipws);
1443 file.open(file_name);
1444 if (file.fail()) {
1445 throw (file_open_exception(file_name));
1446 }
1447 file.get(c);
1448 while (file.good()) {
1449 // Detect the start of a comment.
1450 if (!in_comment && c == '/') {
1451 if (file.peek() == '*') {
1452 file.get(c);
1453 in_comment = true;
1454 comment.clear();
1455 }
1456 else file_contents += c;
1457 }
1458 // Detect the end of a comment.
1459 else if (in_comment && c == '*') {
1460 if (file.peek() == '/') {
1461 file.get(c);
1462 in_comment = false;
1463 comment_blocks.push_back(comment);
1464 }
1465 else comment += c;
1466 }
1467 // Nothings to see. We're just adding to the
1468 // relevant output.
1469 else if (in_comment)
1470 comment += c;
1471 else
1472 file_contents += c;
1473 file.get(c);
1474 }
1475 file.close();
1476}
Exception used by the application in main(...).

◆ show_file_includes()

void TPTPParser::show_file_includes ( )

Show any includes present in the TPTP file.

These are collected as part of the parse.

Definition at line 1884 of file TPTPParser.cpp.

1884 {
1885 for (FileIncludeItem i : file_includes) {
1886 cout << "From " << i.first << ": ";
1887 if (i.second.size() == 0)
1888 cout << "all";
1889 else
1890 for (string s : i.second)
1891 cout << s << " ";
1892 cout << endl;
1893 }
1894}

◆ simplified_fof_has_axioms()

bool TPTPParser::simplified_fof_has_axioms ( ) const

Where there any axioms for an FOF problem after simplification?

Definition at line 2131 of file TPTPParser.cpp.

2131 {
2132 return has_axioms_remaining;
2133}

Member Data Documentation

◆ comment_blocks

vector<string> TPTPParser::comment_blocks
private

Each comment is stored here.

Definition at line 669 of file TPTPParser.hpp.

◆ file_contents

string TPTPParser::file_contents
private

Contents of the TPTP file, with comments removed.

Assuming of course that you used read_tptp_from_file.

Definition at line 665 of file TPTPParser.hpp.

◆ fip

FunctionIndex* TPTPParser::fip
private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 683 of file TPTPParser.hpp.

◆ matrix

Matrix* TPTPParser::matrix
private

The class has a pointer to the matrix, and can therefore construct it as it parses.

Definition at line 702 of file TPTPParser.hpp.

◆ pip

PredicateIndex* TPTPParser::pip
private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 697 of file TPTPParser.hpp.

◆ tip

TermIndex* TPTPParser::tip
private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 690 of file TPTPParser.hpp.

◆ vip

VariableIndex* TPTPParser::vip
private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 676 of file TPTPParser.hpp.


The documentation for this class was generated from the following files: