diff options
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
| -rw-r--r-- | src/parser/tptp/tptp.cpp | 30 |
1 files changed, 21 insertions, 9 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 764e83361..91fcc7a12 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -25,6 +25,7 @@ #include "options/options_public.h" #include "parser/parser.h" #include "smt/command.h" +#include "theory/logic_info.h" // ANTLR defines these, which is really bad! #undef true @@ -37,7 +38,10 @@ Tptp::Tptp(api::Solver* solver, SymbolManager* sm, bool strictMode, bool parseOnly) - : Parser(solver, sm, strictMode, parseOnly), d_cnf(false), d_fof(false) + : Parser(solver, sm, strictMode, parseOnly), + d_cnf(false), + d_fof(false), + d_hol(false) { addTheory(Tptp::THEORY_CORE); @@ -312,21 +316,18 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) isBuiltinKind = true; } Assert(kind != api::NULL_EXPR); - const Options& opts = d_solver->getOptions(); // Second phase: apply parse op to the arguments if (isBuiltinKind) { - if (!options::getUfHo(opts) - && (kind == api::EQUAL || kind == api::DISTINCT)) + if (!hol() && (kind == api::EQUAL || kind == api::DISTINCT)) { - // need --uf-ho if these operators are applied over function args + // need hol if these operators are applied over function args for (std::vector<api::Term>::iterator i = args.begin(); i != args.end(); ++i) { if ((*i).getSort().isFunction()) { - parseError( - "Cannot apply equalty to functions unless --uf-ho is set."); + parseError("Cannot apply equalty to functions unless THF."); } } } @@ -364,9 +365,9 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) unsigned arity = argt.getFunctionArity(); if (args.size() - 1 < arity) { - if (!options::getUfHo(opts)) + if (!hol()) { - parseError("Cannot partially apply functions unless --uf-ho is set."); + parseError("Cannot partially apply functions unless THF."); } Debug("parser") << "Partial application of " << args[0]; Debug("parser") << " : #argTypes = " << arity; @@ -438,6 +439,17 @@ api::Term Tptp::mkDecimal( return d_solver->mkReal(ss.str()); } +bool Tptp::hol() const { return d_hol; } +void Tptp::setHol() +{ + if (d_hol) + { + return; + } + d_hol = true; + d_solver->setLogic("HO_UF"); +} + void Tptp::forceLogic(const std::string& logic) { Parser::forceLogic(logic); |