Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/parser/tptp/tptp.cpp	Lines:	216	266	81.2 %
Date:	2021-08-16	Branches:	300	810	37.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Francois Bobot, Haniel Barbosa
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Definition of TPTP parser.
 */

// Do not #include "parser/antlr_input.h" directly. Rely on the header.
#include "parser/tptp/tptp.h"

#include <algorithm>
#include <set>

#include "api/cpp/cvc5.h"
#include "base/check.h"
#include "options/options.h"
#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
#undef false

namespace cvc5 {
namespace parser {

Tptp::Tptp(api::Solver* solver,
           SymbolManager* sm,
           bool strictMode,
           bool parseOnly)
    : Parser(solver, sm, strictMode, parseOnly),
      d_cnf(false),
      d_fof(false),
      d_hol(false)
{
  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("/");
    }
  }
  d_hasConjecture = false;
}

Tptp::~Tptp() {
  for( unsigned i=0; i<d_in_created.size(); i++ ){
    d_in_created[i]->free(d_in_created[i]);
  }
}

void Tptp::addTheory(Theory theory) {
  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 = d_solver->mkUninterpretedSort(d_unsorted_name);
      preemptCommand(new DeclareSortCommand(d_unsorted_name, 0, d_unsorted));
    }
    // propositionnal
    defineType("Bool", d_solver->getBooleanSort());
    defineVar("$true", d_solver->mkTrue());
    defineVar("$false", d_solver->mkFalse());
    addOperator(api::AND);
    addOperator(api::EQUAL);
    addOperator(api::IMPLIES);
    // addOperator(api::ITE); //only for tff thf
    addOperator(api::NOT);
    addOperator(api::OR);
    addOperator(api::XOR);
    addOperator(api::APPLY_UF);
    //Add quantifiers?
    break;

  default:
    std::stringstream ss;
    ss << "internal error: Tptp::addTheory(): unhandled theory " << theory;
    throw ParserException(ss.str());
  }
}


/* The include are managed in the lexer but called in the parser */
// Inspired by http://www.antlr3.org/api/C/interop.html

bool newInputStream(std::string fileName, pANTLR3_LEXER lexer, std::vector< pANTLR3_INPUT_STREAM >& inc ) {
  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 CVC5_ANTLR3_OLD_INPUT_STREAM
  in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) fileName.c_str());
#else  /* CVC5_ANTLR3_OLD_INPUT_STREAM */
  in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT);
#endif /* CVC5_ANTLR3_OLD_INPUT_STREAM */
  if(in == NULL) {
    Debug("parser") << "Can't open " << fileName << std::endl;
    return false;
  }
  // Same thing as 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.
  //
  inc.push_back( in );

  //TODO what said before
  return true;
}

void Tptp::includeFile(std::string fileName) {
  // security for online version
  if(!canIncludeFile()) {
    parseError("include-file feature was disabled for this run.");
  }

  // Get the lexer
  AntlrInput * ai = static_cast<AntlrInput *>(getInput());
  pANTLR3_LEXER lexer = ai->getAntlr3Lexer();

  // push the inclusion scope; will be popped by our special popCharStream
  // would be necessary for handling symbol filtering in inclusions
  //pushScope();

  // 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 or 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, d_in_created)) {
      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 (environment variable TPTP)");
  };

  std::string tptpDirFileName = d_tptpDir + fileName;
  if(! newInputStream(tptpDirFileName,lexer, d_in_created)) {
    parseError("Couldn't open included file: " + fileName
               + " at " + currentDirFileName + " or " + tptpDirFileName);
  }
}

void Tptp::checkLetBinding(const std::vector<api::Term>& bvlist,
                           api::Term lhs,
                           api::Term rhs,
                           bool formula)
{
  if (lhs.getKind() != api::APPLY_UF)
  {
    parseError("malformed let: LHS must be a flat function application");
  }
  const std::multiset<api::Term> vars{lhs.begin(), lhs.end()};
  if (formula && !lhs.getSort().isBoolean())
  {
    parseError("malformed let: LHS must be formula");
  }
  for (const cvc5::api::Term& var : vars)
  {
    if (var.hasOp())
    {
      parseError("malformed let: LHS must be flat, illegal child: " +
                 var.toString());
    }
  }

  // ensure all let-bound variables appear on the LHS, and appear only once
  for (const api::Term& bound_var : bvlist)
  {
    const size_t count = vars.count(bound_var);
    if (count == 0) {
      parseError(
          "malformed let: LHS must make use of all quantified variables, "
          "missing `" +
          bound_var.toString() + "'");
    } else if (count >= 2) {
      parseError("malformed let: LHS cannot use same bound variable twice: " +
                 bound_var.toString());
    }
  }
}

api::Term Tptp::parseOpToExpr(ParseOp& p)
{
  api::Term expr;
  if (!p.d_expr.isNull())
  {
    return p.d_expr;
  }
  // if it has a kind, it's a builtin one and this function should not have been
  // called
  Assert(p.d_kind == api::NULL_EXPR);
  if (isDeclared(p.d_name))
  {  // already appeared
    expr = getVariable(p.d_name);
  }
  else
  {
    api::Sort t =
        p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
    expr = bindVar(p.d_name, t, true);  // must define at level zero
    preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
  }
  return expr;
}

api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
{
  if (Debug.isOn("parser"))
  {
    Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
    for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
         ++i)
    {
      Debug("parser") << "++ " << *i << std::endl;
    }
  }
  Assert(!args.empty());
  // If operator already defined, just build application
  if (!p.d_expr.isNull())
  {
    // this happens with some arithmetic kinds, which are wrapped around
    // lambdas.
    args.insert(args.begin(), p.d_expr);
    return d_solver->mkTerm(api::APPLY_UF, args);
  }
  bool isBuiltinKind = false;
  // the builtin kind of the overall return expression
  api::Kind kind = api::NULL_EXPR;
  // First phase: piece operator together
  if (p.d_kind == api::NULL_EXPR)
  {
    // A non-built-in function application, get the expression
    api::Term v;
    if (isDeclared(p.d_name))
    {  // already appeared
      v = getVariable(p.d_name);
    }
    else
    {
      std::vector<api::Sort> sorts(args.size(), d_unsorted);
      api::Sort t =
          p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
      t = d_solver->mkFunctionSort(sorts, t);
      v = bindVar(p.d_name, t, true);  // must define at level zero
      preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
    }
    // args might be rationals, in which case we need to create
    // distinct constants of the "unsorted" sort to represent them
    for (size_t i = 0; i < args.size(); ++i)
    {
      if (args[i].getSort().isReal()
          && v.getSort().getFunctionDomainSorts()[i] == d_unsorted)
      {
        args[i] = convertRatToUnsorted(args[i]);
      }
    }
    Assert(!v.isNull());
    checkFunctionLike(v);
    kind = getKindForFunction(v);
    args.insert(args.begin(), v);
  }
  else
  {
    kind = p.d_kind;
    isBuiltinKind = true;
  }
  Assert(kind != api::NULL_EXPR);
  // Second phase: apply parse op to the arguments
  if (isBuiltinKind)
  {
    if (!hol() && (kind == api::EQUAL || kind == api::DISTINCT))
    {
      // 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 THF.");
        }
      }
    }
    if (!strictModeEnabled() && (kind == api::AND || kind == api::OR)
        && args.size() == 1)
    {
      // Unary AND/OR can be replaced with the argument.
      return args[0];
    }
    if (kind == api::MINUS && args.size() == 1)
    {
      return d_solver->mkTerm(api::UMINUS, args[0]);
    }
    if (kind == api::TO_REAL)
    {
      // If the type is real, this is a no-op. We require this special
      // case in the TPTP parser since TO_REAL is designed to match the
      // SMT-LIB operator, meaning it can only be applied to integers, whereas
      // the TPTP to_real / to_rat do not have the same semantics.
      api::Sort s = args[0].getSort();
      if (s.isReal())
      {
        return args[0];
      }
    }
    return d_solver->mkTerm(kind, args);
  }

  // check if partially applied function, in this case we use HO_APPLY
  if (args.size() >= 2)
  {
    api::Sort argt = args[0].getSort();
    if (argt.isFunction())
    {
      unsigned arity = argt.getFunctionArity();
      if (args.size() - 1 < arity)
      {
        if (!hol())
        {
          parseError("Cannot partially apply functions unless THF.");
        }
        Debug("parser") << "Partial application of " << args[0];
        Debug("parser") << " : #argTypes = " << arity;
        Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
        // must curry the partial application
        return d_solver->mkTerm(api::HO_APPLY, args);
      }
    }
  }
  return d_solver->mkTerm(kind, args);
}

api::Term Tptp::mkDecimal(
    std::string& snum, std::string& sden, bool pos, size_t exp, bool posE)
{
  // the numerator and the denominator
  std::stringstream ssn;
  std::stringstream ssd;
  if (exp != 0)
  {
    if (posE)
    {
      // see if we need to pad zeros on the end, e.g. 1.2E5 ---> 120000
      if (exp >= sden.size())
      {
        ssn << snum << sden;
        for (size_t i = 0, nzero = (exp - sden.size()); i < nzero; i++)
        {
          ssn << "0";
        }
        ssd << "0";
      }
      else
      {
        ssn << snum << sden.substr(0, exp);
        ssd << sden.substr(exp);
      }
    }
    else
    {
      // see if we need to pad zeros on the beginning, e.g. 1.2E-5 ---> 0.000012
      if (exp >= snum.size())
      {
        ssn << "0";
        for (size_t i = 0, nzero = (exp - snum.size()); i < nzero; i++)
        {
          ssd << "0";
        }
        ssd << snum << sden;
      }
      else
      {
        ssn << snum.substr(0, exp);
        ssd << snum.substr(exp) << sden;
      }
    }
  }
  else
  {
    ssn << snum;
    ssd << sden;
  }
  std::stringstream ss;
  if (!pos)
  {
    ss << "-";
  }
  ss << ssn.str() << "." << ssd.str();
  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);
  preemptCommand(new SetBenchmarkLogicCommand(logic));
}

void Tptp::addFreeVar(api::Term var)
{
  Assert(cnf());
  d_freeVar.push_back(var);
}

std::vector<api::Term> Tptp::getFreeVar()
{
  Assert(cnf());
  std::vector<api::Term> r;
  r.swap(d_freeVar);
  return r;
}

api::Term Tptp::convertRatToUnsorted(api::Term expr)
{
  // Create the conversion function If they doesn't exists
  if (d_rtu_op.isNull()) {
    api::Sort t;
    // Conversion from rational to unsorted
    t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted);
    d_rtu_op = d_solver->mkConst(t, "$$rtu");
    preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
    // Conversion from unsorted to rational
    t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort());
    d_utr_op = d_solver->mkConst(t, "$$utr");
    preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
  }
  // Add the inverse in order to show that over the elements that
  // appear in the problem there is a bijection between unsorted and
  // rational
  api::Term ret = d_solver->mkTerm(api::APPLY_UF, d_rtu_op, expr);
  if (d_r_converted.find(expr) == d_r_converted.end()) {
    d_r_converted.insert(expr);
    api::Term eq = d_solver->mkTerm(
        api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret));
    preemptCommand(new AssertCommand(eq));
  }
  return api::Term(ret);
}

api::Term Tptp::convertStrToUnsorted(std::string str)
{
  api::Term& e = d_distinct_objects[str];
  if (e.isNull())
  {
    e = d_solver->mkConst(d_unsorted, str);
  }
  return e;
}

api::Term Tptp::mkLambdaWrapper(api::Kind k, api::Sort argType)
{
  Debug("parser") << "mkLambdaWrapper: kind " << k << " and type " << argType
                  << "\n";
  std::vector<api::Term> lvars;
  std::vector<api::Sort> domainTypes = argType.getFunctionDomainSorts();
  for (unsigned i = 0, size = domainTypes.size(); i < size; ++i)
  {
    // the introduced variable is internal (not parsable)
    std::stringstream ss;
    ss << "_lvar_" << i;
    api::Term v = d_solver->mkVar(domainTypes[i], ss.str());
    lvars.push_back(v);
  }
  // apply body of lambda to variables
  api::Term wrapper =
      d_solver->mkTerm(api::LAMBDA,
                       d_solver->mkTerm(api::BOUND_VAR_LIST, lvars),
                       d_solver->mkTerm(k, lvars));

  return wrapper;
}

api::Term Tptp::getAssertionExpr(FormulaRole fr, api::Term expr)
{
  switch (fr) {
    case FR_AXIOM:
    case FR_HYPOTHESIS:
    case FR_DEFINITION:
    case FR_ASSUMPTION:
    case FR_LEMMA:
    case FR_THEOREM:
    case FR_NEGATED_CONJECTURE:
    case FR_PLAIN:
      // it's a usual assert
      return expr;
    case FR_CONJECTURE:
      // it should be negated when asserted
      return d_solver->mkTerm(api::NOT, expr);
    case FR_UNKNOWN:
    case FR_FI_DOMAIN:
    case FR_FI_FUNCTORS:
    case FR_FI_PREDICATES:
    case FR_TYPE:
      // it does not correspond to an assertion
      return d_nullExpr;
      break;
  }
  Assert(false);  // unreachable
  return d_nullExpr;
}

api::Term Tptp::getAssertionDistinctConstants()
{
  std::vector<api::Term> constants;
  for (std::pair<const std::string, api::Term>& cs : d_distinct_objects)
  {
    constants.push_back(cs.second);
  }
  if (constants.size() > 1)
  {
    return d_solver->mkTerm(api::DISTINCT, constants);
  }
  return d_nullExpr;
}

Command* Tptp::makeAssertCommand(FormulaRole fr, api::Term expr, bool cnf)
{
  // For SZS ontology compliance.
  // if we're in cnf() though, conjectures don't result in "Theorem" or
  // "CounterSatisfiable".
  if (!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
    d_hasConjecture = true;
    Assert(!expr.isNull());
  }
  if( expr.isNull() ){
    return new EmptyCommand("Untreated role for expression");
  }else{
    return new AssertCommand(expr);
  }
}

}  // namespace parser
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Francois Bobot, Haniel Barbosa
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Definition of TPTP parser.
14		*/
15
16		// Do not #include "parser/antlr_input.h" directly. Rely on the header.
17		#include "parser/tptp/tptp.h"
18
19		#include <algorithm>
20		#include <set>
21
22		#include "api/cpp/cvc5.h"
23		#include "base/check.h"
24		#include "options/options.h"
25		#include "options/options_public.h"
26		#include "parser/parser.h"
27		#include "smt/command.h"
28		#include "theory/logic_info.h"
29
30		// ANTLR defines these, which is really bad!
31		#undef true
32		#undef false
33
34		namespace cvc5 {
35		namespace parser {
36
37	41	Tptp::Tptp(api::Solver* solver,
38		SymbolManager* sm,
39		bool strictMode,
40	41	bool parseOnly)
41		: Parser(solver, sm, strictMode, parseOnly),
42		d_cnf(false),
43		d_fof(false),
44	41	d_hol(false)
45		{
46	41	addTheory(Tptp::THEORY_CORE);
47
48		/* Try to find TPTP dir */
49		// From tptp4x FileUtilities
50		//----Try the TPTP directory, and TPTP variations
51	41	char* home = getenv("TPTP");
52	41	if(home == NULL) {
53	41	home = getenv("TPTP_HOME");
54		// //----If no TPTP_HOME, try the tptp user (aaargh)
55		// if(home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) {
56		// home = PasswdEntry->pw_dir;
57		// }
58		//----Now look in the TPTP directory from there
59	41	if(home != NULL) {
60		d_tptpDir = home;
61		d_tptpDir.append("/TPTP/");
62		}
63		} else {
64		d_tptpDir = home;
65		//add trailing "/"
66		if(d_tptpDir[d_tptpDir.size() - 1] != '/') {
67		d_tptpDir.append("/");
68		}
69		}
70	41	d_hasConjecture = false;
71	41	}
72
73	123	Tptp::~Tptp() {
74	48	for( unsigned i=0; i<d_in_created.size(); i++ ){
75	7	d_in_created[i]->free(d_in_created[i]);
76		}
77	82	}
78
79	41	void Tptp::addTheory(Theory theory) {
80	41	switch(theory) {
81	41	case THEORY_CORE:
82		//TPTP (CNF and FOF) is unsorted so we define this common type
83		{
84	82	std::string d_unsorted_name = "$$unsorted";
85	41	d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name);
86	82	preemptCommand(new DeclareSortCommand(d_unsorted_name, 0, d_unsorted));
87		}
88		// propositionnal
89	41	defineType("Bool", d_solver->getBooleanSort());
90	41	defineVar("$true", d_solver->mkTrue());
91	41	defineVar("$false", d_solver->mkFalse());
92	41	addOperator(api::AND);
93	41	addOperator(api::EQUAL);
94	41	addOperator(api::IMPLIES);
95		// addOperator(api::ITE); //only for tff thf
96	41	addOperator(api::NOT);
97	41	addOperator(api::OR);
98	41	addOperator(api::XOR);
99	41	addOperator(api::APPLY_UF);
100		//Add quantifiers?
101	41	break;
102
103		default:
104		std::stringstream ss;
105		ss << "internal error: Tptp::addTheory(): unhandled theory " << theory;
106		throw ParserException(ss.str());
107		}
108	41	}
109
110
111		/* The include are managed in the lexer but called in the parser */
112		// Inspired by http://www.antlr3.org/api/C/interop.html
113
114	7	bool newInputStream(std::string fileName, pANTLR3_LEXER lexer, std::vector< pANTLR3_INPUT_STREAM >& inc ) {
115	7	Debug("parser") << "Including " << fileName << std::endl;
116		// Create a new input stream and take advantage of built in stream stacking
117		// in C target runtime.
118		//
119		pANTLR3_INPUT_STREAM in;
120		#ifdef CVC5_ANTLR3_OLD_INPUT_STREAM
121		in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) fileName.c_str());
122		#else /* CVC5_ANTLR3_OLD_INPUT_STREAM */
123	7	in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT);
124		#endif /* CVC5_ANTLR3_OLD_INPUT_STREAM */
125	7	if(in == NULL) {
126		Debug("parser") << "Can't open " << fileName << std::endl;
127		return false;
128		}
129		// Same thing as the predefined PUSHSTREAM(in);
130	7	lexer->pushCharStream(lexer,in);
131		// restart it
132		//lexer->rec->state->tokenStartCharIndex = -10;
133		//lexer->emit(lexer);
134
135		// Note that the input stream is not closed when it EOFs, I don't bother
136		// to do it here, but it is up to you to track streams created like this
137		// and destroy them when the whole parse session is complete. Remember that you
138		// don't want to do this until all tokens have been manipulated all the way through
139		// your tree parsers etc as the token does not store the text it just refers
140		// back to the input stream and trying to get the text for it will abort if you
141		// close the input stream too early.
142		//
143	7	inc.push_back( in );
144
145		//TODO what said before
146	7	return true;
147		}
148
149	7	void Tptp::includeFile(std::string fileName) {
150		// security for online version
151	7	if(!canIncludeFile()) {
152		parseError("include-file feature was disabled for this run.");
153		}
154
155		// Get the lexer
156	7	AntlrInput * ai = static_cast<AntlrInput *>(getInput());
157	7	pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
158
159		// push the inclusion scope; will be popped by our special popCharStream
160		// would be necessary for handling symbol filtering in inclusions
161		//pushScope();
162
163		// get the name of the current stream "Does it work inside an include?"
164	7	const std::string inputName = ai->getInputStreamName();
165
166		// Test in the directory of the actual parsed file
167	7	std::string currentDirFileName;
168	7	if(inputName != "<stdin>") {
169		// TODO: Use dirname or Boost::filesystem?
170	7	size_t pos = inputName.rfind('/');
171	7	if(pos != std::string::npos) {
172		currentDirFileName = std::string(inputName, 0, pos + 1);
173		}
174	7	currentDirFileName.append(fileName);
175	7	if(newInputStream(currentDirFileName,lexer, d_in_created)) {
176	7	return;
177		}
178		} else {
179		currentDirFileName = "<unknown current directory for stdin>";
180		}
181
182		if(d_tptpDir.empty()) {
183		parseError("Couldn't open included file: " + fileName
184		+ " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
185		};
186
187		std::string tptpDirFileName = d_tptpDir + fileName;
188		if(! newInputStream(tptpDirFileName,lexer, d_in_created)) {
189		parseError("Couldn't open included file: " + fileName
190		+ " at " + currentDirFileName + " or " + tptpDirFileName);
191		}
192		}
193
194	3	void Tptp::checkLetBinding(const std::vector<api::Term>& bvlist,
195		api::Term lhs,
196		api::Term rhs,
197		bool formula)
198		{
199	3	if (lhs.getKind() != api::APPLY_UF)
200		{
201		parseError("malformed let: LHS must be a flat function application");
202		}
203	6	const std::multiset<api::Term> vars{lhs.begin(), lhs.end()};
204	3	if (formula && !lhs.getSort().isBoolean())
205		{
206		parseError("malformed let: LHS must be formula");
207		}
208	11	for (const cvc5::api::Term& var : vars)
209		{
210	8	if (var.hasOp())
211		{
212		parseError("malformed let: LHS must be flat, illegal child: " +
213		var.toString());
214		}
215		}
216
217		// ensure all let-bound variables appear on the LHS, and appear only once
218	8	for (const api::Term& bound_var : bvlist)
219		{
220	5	const size_t count = vars.count(bound_var);
221	5	if (count == 0) {
222		parseError(
223		"malformed let: LHS must make use of all quantified variables, "
224		"missing `" +
225		bound_var.toString() + "'");
226	5	} else if (count >= 2) {
227		parseError("malformed let: LHS cannot use same bound variable twice: " +
228		bound_var.toString());
229		}
230		}
231	3	}
232
233	5236	api::Term Tptp::parseOpToExpr(ParseOp& p)
234		{
235	10472	api::Term expr;
236	5236	if (!p.d_expr.isNull())
237		{
238		return p.d_expr;
239		}
240		// if it has a kind, it's a builtin one and this function should not have been
241		// called
242	5236	Assert(p.d_kind == api::NULL_EXPR);
243	5236	if (isDeclared(p.d_name))
244		{ // already appeared
245	5152	expr = getVariable(p.d_name);
246		}
247		else
248		{
249		api::Sort t =
250	168	p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
251	84	expr = bindVar(p.d_name, t, true); // must define at level zero
252	84	preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
253		}
254	5236	return expr;
255		}
256
257	894	api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
258		{
259	894	if (Debug.isOn("parser"))
260		{
261		Debug("parser") << "applyParseOp: " << p << " to:" << std::endl;
262		for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
263		++i)
264		{
265		Debug("parser") << "++ " << *i << std::endl;
266		}
267		}
268	894	Assert(!args.empty());
269		// If operator already defined, just build application
270	894	if (!p.d_expr.isNull())
271		{
272		// this happens with some arithmetic kinds, which are wrapped around
273		// lambdas.
274	27	args.insert(args.begin(), p.d_expr);
275	27	return d_solver->mkTerm(api::APPLY_UF, args);
276		}
277	867	bool isBuiltinKind = false;
278		// the builtin kind of the overall return expression
279	867	api::Kind kind = api::NULL_EXPR;
280		// First phase: piece operator together
281	867	if (p.d_kind == api::NULL_EXPR)
282		{
283		// A non-built-in function application, get the expression
284	1010	api::Term v;
285	505	if (isDeclared(p.d_name))
286		{ // already appeared
287	439	v = getVariable(p.d_name);
288		}
289		else
290		{
291	132	std::vector<api::Sort> sorts(args.size(), d_unsorted);
292		api::Sort t =
293	132	p.d_type == d_solver->getBooleanSort() ? p.d_type : d_unsorted;
294	66	t = d_solver->mkFunctionSort(sorts, t);
295	66	v = bindVar(p.d_name, t, true); // must define at level zero
296	66	preemptCommand(new DeclareFunctionCommand(p.d_name, v, t));
297		}
298		// args might be rationals, in which case we need to create
299		// distinct constants of the "unsorted" sort to represent them
300	1213	for (size_t i = 0; i < args.size(); ++i)
301		{
302	2124	if (args[i].getSort().isReal()
303	2124	&& v.getSort().getFunctionDomainSorts()[i] == d_unsorted)
304		{
305		args[i] = convertRatToUnsorted(args[i]);
306		}
307		}
308	505	Assert(!v.isNull());
309	505	checkFunctionLike(v);
310	505	kind = getKindForFunction(v);
311	505	args.insert(args.begin(), v);
312		}
313		else
314		{
315	362	kind = p.d_kind;
316	362	isBuiltinKind = true;
317		}
318	867	Assert(kind != api::NULL_EXPR);
319		// Second phase: apply parse op to the arguments
320	867	if (isBuiltinKind)
321		{
322	362	if (!hol() && (kind == api::EQUAL \|\| kind == api::DISTINCT))
323		{
324		// need hol if these operators are applied over function args
325	201	for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
326		++i)
327		{
328	134	if ((*i).getSort().isFunction())
329		{
330		parseError("Cannot apply equalty to functions unless THF.");
331		}
332		}
333		}
334	1086	if (!strictModeEnabled() && (kind == api::AND \|\| kind == api::OR)
335	424	&& args.size() == 1)
336		{
337		// Unary AND/OR can be replaced with the argument.
338		return args[0];
339		}
340	362	if (kind == api::MINUS && args.size() == 1)
341		{
342		return d_solver->mkTerm(api::UMINUS, args[0]);
343		}
344	362	if (kind == api::TO_REAL)
345		{
346		// If the type is real, this is a no-op. We require this special
347		// case in the TPTP parser since TO_REAL is designed to match the
348		// SMT-LIB operator, meaning it can only be applied to integers, whereas
349		// the TPTP to_real / to_rat do not have the same semantics.
350	11	api::Sort s = args[0].getSort();
351	8	if (s.isReal())
352		{
353	5	return args[0];
354		}
355		}
356	357	return d_solver->mkTerm(kind, args);
357		}
358
359		// check if partially applied function, in this case we use HO_APPLY
360	505	if (args.size() >= 2)
361		{
362	1010	api::Sort argt = args[0].getSort();
363	505	if (argt.isFunction())
364		{
365	505	unsigned arity = argt.getFunctionArity();
366	505	if (args.size() - 1 < arity)
367		{
368		if (!hol())
369		{
370		parseError("Cannot partially apply functions unless THF.");
371		}
372		Debug("parser") << "Partial application of " << args[0];
373		Debug("parser") << " : #argTypes = " << arity;
374		Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
375		// must curry the partial application
376		return d_solver->mkTerm(api::HO_APPLY, args);
377		}
378		}
379		}
380	505	return d_solver->mkTerm(kind, args);
381		}
382
383	70	api::Term Tptp::mkDecimal(
384		std::string& snum, std::string& sden, bool pos, size_t exp, bool posE)
385		{
386		// the numerator and the denominator
387	140	std::stringstream ssn;
388	140	std::stringstream ssd;
389	70	if (exp != 0)
390		{
391	16	if (posE)
392		{
393		// see if we need to pad zeros on the end, e.g. 1.2E5 ---> 120000
394	10	if (exp >= sden.size())
395		{
396	10	ssn << snum << sden;
397	4953	for (size_t i = 0, nzero = (exp - sden.size()); i < nzero; i++)
398		{
399	4943	ssn << "0";
400		}
401	10	ssd << "0";
402		}
403		else
404		{
405		ssn << snum << sden.substr(0, exp);
406		ssd << sden.substr(exp);
407		}
408		}
409		else
410		{
411		// see if we need to pad zeros on the beginning, e.g. 1.2E-5 ---> 0.000012
412	6	if (exp >= snum.size())
413		{
414	6	ssn << "0";
415	3300	for (size_t i = 0, nzero = (exp - snum.size()); i < nzero; i++)
416		{
417	3294	ssd << "0";
418		}
419	6	ssd << snum << sden;
420		}
421		else
422		{
423		ssn << snum.substr(0, exp);
424		ssd << snum.substr(exp) << sden;
425		}
426		}
427		}
428		else
429		{
430	54	ssn << snum;
431	54	ssd << sden;
432		}
433	140	std::stringstream ss;
434	70	if (!pos)
435		{
436	11	ss << "-";
437		}
438	70	ss << ssn.str() << "." << ssd.str();
439	140	return d_solver->mkReal(ss.str());
440		}
441
442	362	bool Tptp::hol() const { return d_hol; }
443	1315	void Tptp::setHol()
444		{
445	1315	if (d_hol)
446		{
447	1304	return;
448		}
449	11	d_hol = true;
450	11	d_solver->setLogic("HO_UF");
451		}
452
453	1	void Tptp::forceLogic(const std::string& logic)
454		{
455	1	Parser::forceLogic(logic);
456	1	preemptCommand(new SetBenchmarkLogicCommand(logic));
457	1	}
458
459	59	void Tptp::addFreeVar(api::Term var)
460		{
461	59	Assert(cnf());
462	59	d_freeVar.push_back(var);
463	59	}
464
465	85	std::vector<api::Term> Tptp::getFreeVar()
466		{
467	85	Assert(cnf());
468	85	std::vector<api::Term> r;
469	85	r.swap(d_freeVar);
470	85	return r;
471		}
472
473	42	api::Term Tptp::convertRatToUnsorted(api::Term expr)
474		{
475		// Create the conversion function If they doesn't exists
476	42	if (d_rtu_op.isNull()) {
477	12	api::Sort t;
478		// Conversion from rational to unsorted
479	6	t = d_solver->mkFunctionSort(d_solver->getRealSort(), d_unsorted);
480	6	d_rtu_op = d_solver->mkConst(t, "$$rtu");
481	6	preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
482		// Conversion from unsorted to rational
483	6	t = d_solver->mkFunctionSort(d_unsorted, d_solver->getRealSort());
484	6	d_utr_op = d_solver->mkConst(t, "$$utr");
485	6	preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
486		}
487		// Add the inverse in order to show that over the elements that
488		// appear in the problem there is a bijection between unsorted and
489		// rational
490	84	api::Term ret = d_solver->mkTerm(api::APPLY_UF, d_rtu_op, expr);
491	42	if (d_r_converted.find(expr) == d_r_converted.end()) {
492	32	d_r_converted.insert(expr);
493	32	api::Term eq = d_solver->mkTerm(
494	64	api::EQUAL, expr, d_solver->mkTerm(api::APPLY_UF, d_utr_op, ret));
495	32	preemptCommand(new AssertCommand(eq));
496		}
497	84	return api::Term(ret);
498		}
499
500	6	api::Term Tptp::convertStrToUnsorted(std::string str)
501		{
502	6	api::Term& e = d_distinct_objects[str];
503	6	if (e.isNull())
504		{
505	6	e = d_solver->mkConst(d_unsorted, str);
506		}
507	6	return e;
508		}
509
510	1	api::Term Tptp::mkLambdaWrapper(api::Kind k, api::Sort argType)
511		{
512	2	Debug("parser") << "mkLambdaWrapper: kind " << k << " and type " << argType
513	1	<< "\n";
514	2	std::vector<api::Term> lvars;
515	2	std::vector<api::Sort> domainTypes = argType.getFunctionDomainSorts();
516	2	for (unsigned i = 0, size = domainTypes.size(); i < size; ++i)
517		{
518		// the introduced variable is internal (not parsable)
519	2	std::stringstream ss;
520	1	ss << "_lvar_" << i;
521	2	api::Term v = d_solver->mkVar(domainTypes[i], ss.str());
522	1	lvars.push_back(v);
523		}
524		// apply body of lambda to variables
525		api::Term wrapper =
526	1	d_solver->mkTerm(api::LAMBDA,
527	2	d_solver->mkTerm(api::BOUND_VAR_LIST, lvars),
528	3	d_solver->mkTerm(k, lvars));
529
530	2	return wrapper;
531		}
532
533	1311	api::Term Tptp::getAssertionExpr(FormulaRole fr, api::Term expr)
534		{
535	1311	switch (fr) {
536	1286	case FR_AXIOM:
537		case FR_HYPOTHESIS:
538		case FR_DEFINITION:
539		case FR_ASSUMPTION:
540		case FR_LEMMA:
541		case FR_THEOREM:
542		case FR_NEGATED_CONJECTURE:
543		case FR_PLAIN:
544		// it's a usual assert
545	1286	return expr;
546	22	case FR_CONJECTURE:
547		// it should be negated when asserted
548	22	return d_solver->mkTerm(api::NOT, expr);
549	3	case FR_UNKNOWN:
550		case FR_FI_DOMAIN:
551		case FR_FI_FUNCTORS:
552		case FR_FI_PREDICATES:
553		case FR_TYPE:
554		// it does not correspond to an assertion
555	3	return d_nullExpr;
556		break;
557		}
558		Assert(false); // unreachable
559		return d_nullExpr;
560		}
561
562	41	api::Term Tptp::getAssertionDistinctConstants()
563		{
564	82	std::vector<api::Term> constants;
565	47	for (std::pair<const std::string, api::Term>& cs : d_distinct_objects)
566		{
567	6	constants.push_back(cs.second);
568		}
569	41	if (constants.size() > 1)
570		{
571	3	return d_solver->mkTerm(api::DISTINCT, constants);
572		}
573	38	return d_nullExpr;
574		}
575
576	1311	Command* Tptp::makeAssertCommand(FormulaRole fr, api::Term expr, bool cnf)
577		{
578		// For SZS ontology compliance.
579		// if we're in cnf() though, conjectures don't result in "Theorem" or
580		// "CounterSatisfiable".
581	1311	if (!cnf && (fr == FR_NEGATED_CONJECTURE \|\| fr == FR_CONJECTURE)) {
582	22	d_hasConjecture = true;
583	22	Assert(!expr.isNull());
584		}
585	1311	if( expr.isNull() ){
586	3	return new EmptyCommand("Untreated role for expression");
587		}else{
588	1308	return new AssertCommand(expr);
589		}
590		}
591
592		} // namespace parser
593	29325	} // namespace cvc5