diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-18 15:19:10 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-18 15:19:10 -0500 |
commit | 9af7e38d6f0b3d01dea795a4847153047ac87f6e (patch) | |
tree | f16aed9383cead45ea321229560533f3c94b9566 /src/parser/tptp/tptp.h | |
parent | 6f18015fdcb824f46b969882aa45187b46306e97 (diff) |
Tptp unsat cores (#1228)
* Support unsat cores for TPTP.
* Fix assertion
Diffstat (limited to 'src/parser/tptp/tptp.h')
-rw-r--r-- | src/parser/tptp/tptp.h | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index e6d7bbb47..1cc9c2d7f 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -91,7 +91,20 @@ class Tptp : public Parser { void makeApplication(Expr& expr, std::string& name, std::vector<Expr>& args, bool term); - Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf); + /** get assertion expression, based on the formula role. + * expr should have Boolean type. + * This returns the expression that should be asserted, given the formula role fr. + * For example, if the role is "conjecture", then the return value is the negation of expr. + */ + Expr getAssertionExpr(FormulaRole fr, Expr expr); + + /** returns the appropriate AssertCommand, given a role, expression expr to assert, + * and information about the assertion. + * The assertion expr is literally what should be asserted (it is already been processed + * with getAssertionExpr above). + * This may set a flag in the parser to mark that we have asserted a conjecture. + */ + Command* makeAssertCommand(FormulaRole fr, Expr expr, bool cnf, bool inUnsatCore); /** Ugly hack because I don't know how to return an expression from a token */ @@ -124,6 +137,9 @@ class Tptp : public Parser { // TPTP directory where to find includes; // empty if none could be determined std::string d_tptpDir; + + // the null expression + Expr d_nullExpr; // hack to make output SZS ontology-compliant bool d_hasConjecture; |