diff options
author | François Bobot <francois@bobot.eu> | 2012-06-22 15:11:37 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-06-22 15:11:37 +0000 |
commit | 84c4269f3b9edb8de4134fe464dfc70679da2bb1 (patch) | |
tree | b0c8f33e04d925064ffa9d85f1caeb6a3ff745b2 /src/parser/tptp/tptp.cpp | |
parent | eda7d4df5481030d4e9cb6ef4a33d52afc8f7e0a (diff) |
TPTP: add parser for cnf and fof
- include directive works
- no keyword : 'fof', 'cnf', ... can be used for symbols name
- real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted)
- same thing for string
But:
- string not distinct by projection to real, not sure if the current state of string theory make them distinct
- filtering in include is not done
- the result is not printed in the TPTP way (currently SMT2 way)
Diffstat (limited to 'src/parser/tptp/tptp.cpp')
-rw-r--r-- | src/parser/tptp/tptp.cpp | 162 |
1 files changed, 162 insertions, 0 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp new file mode 100644 index 000000000..065c62824 --- /dev/null +++ b/src/parser/tptp/tptp.cpp @@ -0,0 +1,162 @@ +/********************* */ +/*! \file tptp.cpp + ** \verbatim + ** Original author: cconway + ** Major contributors: mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definitions of TPTP constants. + ** + ** Definitions of TPTP constants. + **/ + +#include "expr/type.h" +#include "parser/parser.h" +#include "parser/smt/smt.h" +#include "parser/tptp/tptp.h" +#include "parser/antlr_input.h" + +namespace CVC4 { +namespace parser { + +Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) : + Parser(exprManager,input,strictMode,parseOnly) { + addTheory(Tptp::THEORY_CORE); + + /* Try to find TPTP dir */ + // From tptp4x FileUtilities + //----Try the TPTP directory, and TPTP variations + char* home = getenv("TPTP"); + if (home == NULL) { + home = getenv("TPTP_HOME"); +// //----If no TPTP_HOME, try the tptp user (aaargh) +// if (home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) { +// home = PasswdEntry->pw_dir; +// } +//----Now look in the TPTP directory from there + if (home != NULL) { + d_tptpDir = home; + d_tptpDir.append("/TPTP/"); + } + } else { + d_tptpDir = home; + //add trailing "/" + if( d_tptpDir[d_tptpDir.size() - 1] != '/'){ + d_tptpDir.append("/"); + } + } +} + +void Tptp::addTheory(Theory theory) { + ExprManager * em = getExprManager(); + switch(theory) { + case THEORY_CORE: + //TPTP (CNF and FOF) is unsorted so we define this common type + { + std::string d_unsorted_name = "$$unsorted"; + d_unsorted = em->mkSort(d_unsorted_name); + preemptCommand( new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted) ); + } + // propositionnal + defineType("Bool", em->booleanType()); + defineVar("$true", em->mkConst(true)); + defineVar("$false", em->mkConst(false)); + addOperator(kind::AND); + addOperator(kind::EQUAL); + addOperator(kind::IFF); + addOperator(kind::IMPLIES); + //addOperator(kind::ITE); //only for tff thf + addOperator(kind::NOT); + addOperator(kind::OR); + addOperator(kind::XOR); + addOperator(kind::APPLY_UF); + //Add quantifiers? + break; + + default: + Unhandled(theory); + } +} + + +/* The include are managed in the lexer but called in the parser */ +// Inspired by http://www.antlr.org/api/C/interop.html + +bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){ + Debug("parser") << "Including " << fileName << std::endl; + // Create a new input stream and take advantage of built in stream stacking + // in C target runtime. + // + pANTLR3_INPUT_STREAM in; +#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM + in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) fileName.c_str()); +#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT); +#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */ + if( in == NULL ) { + Debug("parser") << "Can't open " << fileName << std::endl; + return false; + } + // Samething than the predefined PUSHSTREAM(in); + lexer->pushCharStream(lexer,in); + // restart it + //lexer->rec->state->tokenStartCharIndex = -10; + //lexer->emit(lexer); + + // Note that the input stream is not closed when it EOFs, I don't bother + // to do it here, but it is up to you to track streams created like this + // and destroy them when the whole parse session is complete. Remember that you + // don't want to do this until all tokens have been manipulated all the way through + // your tree parsers etc as the token does not store the text it just refers + // back to the input stream and trying to get the text for it will abort if you + // close the input stream too early. + // + + //TODO what said before + return true; +} + + +void Tptp::includeFile(std::string fileName){ + // Get the lexer + AntlrInput * ai = static_cast<AntlrInput *>(getInput()); + pANTLR3_LEXER lexer = ai->getAntlr3Lexer(); + // get the name of the current stream "Does it work inside an include?" + const std::string inputName = ai->getInputStreamName(); + + // Test in the directory of the actual parsed file + std::string currentDirFileName; + if( inputName != "<stdin>"){ + // TODO: Use dirname ot Boost::filesystem? + size_t pos = inputName.rfind('/'); + if( pos != std::string::npos){ + currentDirFileName = std::string(inputName, 0, pos + 1); + } + currentDirFileName.append(fileName); + if( newInputStream(currentDirFileName,lexer) ){ + return; + } + } else { + currentDirFileName = "<unknown current directory for stdin>"; + } + + if( d_tptpDir.empty() ){ + parseError("Couldn't open included file: " + fileName + + " at " + currentDirFileName + " and the TPTP directory is not specified (environnement variable TPTP)"); + }; + + std::string tptpDirFileName = d_tptpDir + fileName; + if( !newInputStream(tptpDirFileName,lexer) ){ + parseError("Couldn't open included file: " + fileName + + " at " + currentDirFileName + " or " + tptpDirFileName); + } +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ |