=================
* SMT-LIB support for abs, to_real, to_int, is_int
+* Expr::substitute() now capable of substituting operators (e.g.,
+ function symbols under an APPLY_UF)
* Support in linear logics for /, div, and mod by constants.
+* Support for TPTP's TFF and TFA formats.
* We no longer permit model or proof generation if there's been an
intervening push/pop.
* Increased compliance to SMT-LIBv2, numerous bugs and usability issues
Expr ExprManager::mkExpr(Expr opExpr) {
const unsigned n = 0;
- Kind kind = kind::operatorKindToKind(opExpr.getKind());
- CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
"This Expr constructor is for parameterized kinds only");
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
Expr ExprManager::mkExpr(Expr opExpr, Expr child1) {
const unsigned n = 1;
- Kind kind = kind::operatorKindToKind(opExpr.getKind());
- CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
"This Expr constructor is for parameterized kinds only");
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) {
const unsigned n = 2;
- Kind kind = kind::operatorKindToKind(opExpr.getKind());
- CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
"This Expr constructor is for parameterized kinds only");
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) {
const unsigned n = 3;
- Kind kind = kind::operatorKindToKind(opExpr.getKind());
- CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
"This Expr constructor is for parameterized kinds only");
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
Expr child4) {
const unsigned n = 4;
- Kind kind = kind::operatorKindToKind(opExpr.getKind());
- CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
"This Expr constructor is for parameterized kinds only");
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3,
Expr child4, Expr child5) {
const unsigned n = 5;
- Kind kind = kind::operatorKindToKind(opExpr.getKind());
- CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
"This Expr constructor is for parameterized kinds only");
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
const unsigned n = children.size();
- Kind kind = kind::operatorKindToKind(opExpr.getKind());
- CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
+ Kind kind = NodeManager::operatorToKind(opExpr.getNode());
+ CheckArgument(opExpr.getKind() == kind::BUILTIN || kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr,
"This Expr constructor is for parameterized kinds only");
CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind,
"Exprs with kind %s must have at least %u children and "
return metaKinds[k + 1];
}/* metaKindOf(k) */
-/**
- * Map a kind of the operator to the kind of the enclosing expression. For
- * example, since the kind of functions is just VARIABLE, it should map
- * VARIABLE to APPLY_UF.
- */
-static inline Kind operatorKindToKind(Kind k) {
- switch (k) {
-${metakind_operatorKinds}
- default:
- return kind::UNDEFINED_KIND; /* LAST_KIND */
- };
-}
}/* CVC4::kind namespace */
namespace expr {
}
}/* CVC4::kind::metakind namespace */
+
+/**
+ * Map a kind of the operator to the kind of the enclosing expression. For
+ * example, since the kind of functions is just VARIABLE, it should map
+ * VARIABLE to APPLY_UF.
+ */
+static inline Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
+ if(nv->getKind() == kind::BUILTIN) {
+ return nv->getConst<Kind>();
+ } else if(nv->getKind() == kind::LAMBDA) {
+ return kind::APPLY_UF;
+ }
+
+ switch(Kind k CVC4_UNUSED = nv->getKind()) {
+${metakind_operatorKinds}
+ default:
+ return kind::UNDEFINED_KIND; /* LAST_KIND */
+ };
+}
+
}/* CVC4::kind namespace */
-#line 330 "${template}"
+#line 338 "${template}"
namespace theory {
NodeBuilder<> nb(getKind());
if(getMetaKind() == kind::metakind::PARAMETERIZED) {
// push the operator
- nb << getOperator();
+ if(getOperator() == node) {
+ nb << replacement;
+ } else {
+ nb << getOperator().substitute(node, replacement, cache);
+ }
}
for(const_iterator i = begin(),
iend = end();
Assert(!isUsed(), "NodeBuilder is one-shot only; "
"attempt to access it after conversion");
Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node");
+ if(n.getKind() == kind::BUILTIN) {
+ return *this << NodeManager::operatorToKind(n);
+ }
allocateNvIfNecessaryForAppend();
expr::NodeValue* nv = n.d_nv;
nv->inc();
#if 0
// if the kind is PARAMETERIZED, check that the operator is correctly-kinded
Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
- kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+ NodeManager::operatorToKind(getOperator()) == getKind(),
"Attempted to construct a parameterized kind `%s' with "
"incorrectly-kinded operator `%s'",
kind::kindToString(getKind()).c_str(),
#if 0
// if the kind is PARAMETERIZED, check that the operator is correctly-kinded
Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED ||
- kind::operatorKindToKind(getOperator().getKind()) == getKind(),
+ NodeManager::operatorToKind(getOperator()) == getKind(),
"Attempted to construct a parameterized kind `%s' with "
"incorrectly-kinded operator `%s'",
kind::kindToString(getKind()).c_str(),
d_listeners.erase(elt);
}
+ /** Get a Kind from an operator expression */
+ static inline Kind operatorToKind(TNode n);
+
// general expression-builders
/** Create a node with one child. */
return type;
}
+inline Kind NodeManager::operatorToKind(TNode n) {
+ return kind::operatorToKind(n.d_nv);
+}
+
inline Node NodeManager::mkNode(Kind kind, TNode child1) {
NodeBuilder<1> nb(this, kind);
nb << child1;
// for operators
inline Node NodeManager::mkNode(TNode opNode) {
- NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<1> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode) {
- NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<1> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
- NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1;
+ NodeBuilder<2> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
- NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1;
+ NodeBuilder<2> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
- NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2;
+ NodeBuilder<3> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
- NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2;
+ NodeBuilder<3> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
TNode child3) {
- NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3;
+ NodeBuilder<4> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
TNode child3) {
- NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3;
+ NodeBuilder<4> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4) {
- NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4;
+ NodeBuilder<5> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4) {
- NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4;
+ NodeBuilder<5> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4, TNode child5) {
- NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4 << child5;
+ NodeBuilder<6> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4 << child5;
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
TNode child3, TNode child4, TNode child5) {
- NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode << child1 << child2 << child3 << child4 << child5;
+ NodeBuilder<6> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
+ nb << child1 << child2 << child3 << child4 << child5;
return nb.constructNodePtr();
}
inline Node NodeManager::mkNode(TNode opNode,
const std::vector<NodeTemplate<ref_count> >&
children) {
- NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
nb.append(children);
return nb.constructNode();
}
inline Node* NodeManager::mkNodePtr(TNode opNode,
const std::vector<NodeTemplate<ref_count> >&
children) {
- NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
- nb << opNode;
+ NodeBuilder<> nb(this, operatorToKind(opNode));
+ if(opNode.getKind() != kind::BUILTIN) {
+ nb << opNode;
+ }
nb.append(children);
return nb.constructNodePtr();
}
return d_typeNode->isSubrange();
}
+size_t FunctionType::getArity() const {
+ return d_typeNode->getNumChildren() - 1;
+}
+
vector<Type> FunctionType::getArgTypes() const {
NodeManagerScope nms(d_nodeManager);
vector<Type> args;
/** Construct from the base type */
FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
+ /** Get the arity of the function type */
+ size_t getArity() const;
+
/** Get the argument types */
std::vector<Type> getArgTypes() const;
namespace CVC4 {
namespace main {
-CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options):
+CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
d_exprMgr(exprMgr),
d_smtEngine(SmtEngine(&exprMgr)),
d_options(options),
- d_stats("driver") {
+ d_stats("driver"),
+ d_result() {
}
bool CommandExecutor::doCommand(Command* cmd)
}
}
-bool CommandExecutor::doCommandSingleton(Command *cmd)
+bool CommandExecutor::doCommandSingleton(Command* cmd)
{
bool status = true;
if(d_options[options::verbosity] >= -1) {
} else {
status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
}
- //dump the model if option is set
- if(status && d_options[options::produceModels] && d_options[options::dumpModels]) {
- CheckSatCommand *cs = dynamic_cast<CheckSatCommand*>(cmd);
- if(cs != NULL) {
- if(cs->getResult().asSatisfiabilityResult().isSat() == Result::SAT ||
- (cs->getResult().isUnknown() && cs->getResult().whyUnknown() == Result::INCOMPLETE) ){
- Command * gm = new GetModelCommand;
- status = doCommandSingleton(gm);
- }
- }
+ Result res;
+ CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+ if(cs != NULL) {
+ d_result = res = cs->getResult();
+ }
+ QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+ if(q != NULL) {
+ d_result = res = q->getResult();
+ }
+ // dump the model if option is set
+ if( status &&
+ d_options[options::produceModels] &&
+ d_options[options::dumpModels] &&
+ ( res.asSatisfiabilityResult() == Result::SAT ||
+ (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+ Command* gm = new GetModelCommand();
+ status = doCommandSingleton(gm);
}
return status;
}
-std::string CommandExecutor::getSmtEngineStatus()
-{
- return d_smtEngine.getInfo("status").getValue();
-}
-
bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
{
if(out == NULL) {
SmtEngine d_smtEngine;
Options& d_options;
StatisticsRegistry d_stats;
+ Result d_result;
public:
CommandExecutor(ExprManager &exprMgr, Options &options);
*/
bool doCommand(CVC4::Command* cmd);
- virtual std::string getSmtEngineStatus();
+ Result getResult() const { return d_result; }
StatisticsRegistry& getStatisticsRegistry() {
return d_stats;
// command
if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
- dynamic_cast<QueryCommand*>(cmd) != NULL) {
+ dynamic_cast<QueryCommand*>(cmd) != NULL) {
mode = 1;
} else if(dynamic_cast<GetValueCommand*>(cmd) != NULL ||
dynamic_cast<GetAssignmentCommand*>(cmd) != NULL ||
d_lastWinner = portfolioReturn.first;
+ CheckSatCommand* cs = dynamic_cast<CheckSatCommand*>(cmd);
+ if(cs != NULL) {
+ d_result = cs->getResult();
+ }
+ QueryCommand* q = dynamic_cast<QueryCommand*>(cmd);
+ if(q != NULL) {
+ d_result = q->getResult();
+ }
+ dynamic_cast<QueryCommand*>(cmd) != NULL) {
+
if(d_ostringstreams.size() != 0) {
assert(d_numThreads == d_options[options::threads]);
assert(portfolioReturn.first >= 0);
}/* CommandExecutorPortfolio::doCommandSingleton() */
-std::string CommandExecutorPortfolio::getSmtEngineStatus()
-{
- return d_smts[d_lastWinner]->getInfo("status").getValue();
-}
-
void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
for(size_t i = 0; i < d_numThreads; ++i) {
opts.set(options::replayStream, NULL);
}
- string result = "unknown";
+ Result result;
if(status) {
- result = pExecutor->getSmtEngineStatus();
+ result = pExecutor->getResult();
- if(result == "sat") {
+ if(result.asSatisfiabilityResult() == Result::SAT) {
returnValue = 10;
- } else if(result == "unsat") {
+ } else if(result.asSatisfiabilityResult() == Result::UNSAT) {
returnValue = 20;
} else {
returnValue = 0;
option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
disable ALL semantic checks, including type checks
-option szsCompliant --szs-compliant bool :default false
- temporary support for szs ontolotogy, print if conjecture is found
-
# this is just to support security in the online version
# (--no-include-file disables filesystem access in TPTP and SMT2 parsers)
undocumented-option canIncludeFile /--no-include-file bool :default true
parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
break;
case language::input::LANG_TPTP:
- {
- Tptp * tparser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
- tparser->d_szsCompliant = d_szsCompliant;
- parser = tparser;
- }
+ parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
break;
default:
parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
}
ParserBuilder& ParserBuilder::withOptions(const Options& options) {
- d_szsCompliant = options[options::szsCompliant];
return
withInputLanguage(options[options::inputLanguage])
.withMmap(options[options::memoryMap])
/** Are we parsing only? */
bool d_parseOnly;
- /** hack for szs compliance */
- bool d_szsCompliant;
-
/** Initialize this parser builder */
void init(ExprManager* exprManager, const std::string& filename);
kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
args.size() > 2 ) {
/* "chainable", but CVC4 internally only supports 2 args */
- expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args);
+ expr = MK_EXPR(MK_CONST(Chain(kind)), args);
} else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
args.size() == 1 && !args[0].getType().isInteger() ) {
/* first, check that ABS is even defined in this logic */
// Only lookahead of <= k requested (disable for LL* parsing)
// Note that CVC4's BoundedTokenBuffer requires a fixed k !
// If you change this k, change it also in tptp_input.cpp !
- k = 1;
+ k = 2;
}/* options */
@header {
#include "util/output.h"
#include "util/rational.h"
#include <vector>
+#include <iterator>
+#include <algorithm>
using namespace CVC4;
using namespace CVC4::parser;
#define EXPR_MANAGER PARSER_STATE->getExprManager()
#undef MK_EXPR
#define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_EXPR_ASSOCIATIVE
+#define MK_EXPR_ASSOCIATIVE EXPR_MANAGER->mkAssociative
#undef MK_CONST
#define MK_CONST EXPR_MANAGER->mkConst
#define UNSUPPORTED PARSER_STATE->unimplementedFeature
-
-
}/* parser::postinclude */
/**
@declarations {
Expr expr;
Tptp::FormulaRole fr;
- std::string name;
- std::string incl_args;
+ std::string name, inclSymbol;
}
// : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
: CNF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
- { PARSER_STATE->cnf=true; PARSER_STATE->pushScope(); }
+ { PARSER_STATE->cnf = true; PARSER_STATE->fof = false; PARSER_STATE->pushScope(); }
cnfFormula[expr]
{ PARSER_STATE->popScope();
std::vector<Expr> bvl = PARSER_STATE->getFreeVar();
- if(!bvl.empty()){
+ if(!bvl.empty()) {
expr = MK_EXPR(kind::FORALL,MK_EXPR(kind::BOUND_VAR_LIST,bvl),expr);
};
}
(COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
{
- cmd = PARSER_STATE->makeCommand(fr,expr);
+ cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ true);
}
| FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
- { PARSER_STATE->cnf=false; }
+ { PARSER_STATE->cnf = false; PARSER_STATE->fof = true; }
fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
{
- cmd = PARSER_STATE->makeCommand(fr,expr);
+ cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
}
+ | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK
+ ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd]
+ | formulaRole[fr] COMMA_TOK
+ { PARSER_STATE->cnf = false; PARSER_STATE->fof = false; }
+ tffFormula[expr] (COMMA_TOK anything*)?
+ {
+ cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
+ }
+ ) RPAREN_TOK DOT_TOK
| INCLUDE_TOK LPAREN_TOK unquotedFileName[name]
- ( COMMA_TOK LBRACK_TOK nameN[incl_args] ( COMMA_TOK nameN[incl_args] )* RBRACK_TOK )?
+ ( COMMA_TOK LBRACK_TOK nameN[inclSymbol]
+ ( COMMA_TOK nameN[inclSymbol] )* RBRACK_TOK )?
RPAREN_TOK DOT_TOK
- {
- PARSER_STATE->includeFile(name);
- // The command of the included file will be produce at the new parseCommand call
+ { /* TODO - implement symbol filtering for file inclusion.
+ * the following removes duplicates and "all", just need to pass it
+ * through to includeFile() and implement it there.
+ std::sort(inclArgs.begin(), inclArgs.end());
+ std::vector<std::string>::iterator it =
+ std::unique(inclArgs.begin(), inclArgs.end());
+ inclArgs.resize(std::distance(inclArgs.begin(), it));
+ it = std::lower_bound(inclArgs.begin(), inclArgs.end(), std::string("all"));
+ if(it != inclArgs.end() && *it == "all") {
+ inclArgs.erase(it);
+ }
+ */
+ PARSER_STATE->includeFile(name /* , inclArgs */ );
+ // The command of the included file will be produced at the new parseCommand call
cmd = new EmptyCommand("include::" + name);
}
| EOF
{
- PARSER_STATE->preemptCommand(new CheckSatCommand(MK_CONST(bool(true))));
+ std::string filename = PARSER_STATE->getInput()->getInputStreamName();
+ size_t i = filename.find_last_of('/');
+ if(i != std::string::npos) {
+ filename = filename.substr(i + 1);
+ }
+ if(filename.substr(filename.length() - 2) == ".p") {
+ filename = filename.substr(0, filename.length() - 2);
+ }
+ CommandSequence* seq = new CommandSequence();
+ seq->addCommand(new SetInfoCommand("name", filename));
+ if(PARSER_STATE->hasConjecture()) {
+ seq->addCommand(new QueryCommand(MK_CONST(bool(false))));
+ } else {
+ seq->addCommand(new CheckSatCommand());
+ }
+ PARSER_STATE->preemptCommand(seq);
cmd = NULL;
}
;
/* Parse a formula Role */
-formulaRole[CVC4::parser::Tptp::FormulaRole & role]
+formulaRole[CVC4::parser::Tptp::FormulaRole& role]
: LOWER_WORD
{
std::string r = AntlrInput::tokenText($LOWER_WORD);
/* CNF */
/* It can parse a little more than the cnf grammar: false and true can appear.
- Normally only false can appear and only at top level
-*/
+ * Normally only false can appear and only at top level. */
cnfFormula[CVC4::Expr& expr]
- :
- LPAREN_TOK disjunction[expr] RPAREN_TOK
-| disjunction[expr]
+ : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK
+ | cnfDisjunction[expr]
//| FALSE_TOK { expr = MK_CONST(bool(false)); }
;
-disjunction[CVC4::Expr& expr]
+cnfDisjunction[CVC4::Expr& expr]
@declarations {
std::vector<Expr> args;
}
- :
- literal[expr] {args.push_back(expr); } ( OR_TOK literal[expr] {args.push_back(expr); } )*
- {
- if(args.size() > 1){
- expr = MK_EXPR(kind::OR,args);
+ : cnfLiteral[expr] { args.push_back(expr); }
+ ( OR_TOK cnfLiteral[expr] { args.push_back(expr); } )*
+ { if(args.size() > 1) {
+ expr = MK_EXPR_ASSOCIATIVE(kind::OR, args);
} // else its already in the expr
}
;
-literal[CVC4::Expr& expr]
+cnfLiteral[CVC4::Expr& expr]
: atomicFormula[expr]
- | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
-// | folInfixUnary[expr]
+ | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT, expr); }
+//| folInfixUnary[expr]
;
atomicFormula[CVC4::Expr& expr]
bool equal;
}
: atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
- ( ( equalOp[equal] //equality/disequality between terms
- {
- PARSER_STATE->makeApplication(expr,name,args,true);
- }
- term[expr2]
- {
- expr = MK_EXPR(kind::EQUAL, expr, expr2);
- if(!equal) expr = MK_EXPR(kind::NOT,expr);
- }
- )
- | //predicate
- {
- PARSER_STATE->makeApplication(expr,name,args,false);
+ ( equalOp[equal] term[expr2]
+ { // equality/disequality between terms
+ PARSER_STATE->makeApplication(expr, name, args, true);
+ expr = MK_EXPR(kind::EQUAL, expr, expr2);
+ if(!equal) expr = MK_EXPR(kind::NOT, expr);
}
- )
- | simpleTerm[expr] equalOp[equal] term[expr2]
- {
+ | { // predicate
+ PARSER_STATE->makeApplication(expr, name, args, false);
+ }
+ )
+ | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+ equalOp[equal] term[expr2]
+ { expr = EXPR_MANAGER->mkExpr(expr, args);
+ expr = MK_EXPR(kind::EQUAL, expr, expr2);
+ if(!equal) expr = MK_EXPR(kind::NOT, expr);
+ }
+ | (simpleTerm[expr] | letTerm[expr] | conditionalTerm[expr])
+ equalOp[equal] term[expr2]
+ { // equality/disequality between terms
expr = MK_EXPR(kind::EQUAL, expr, expr2);
- if(!equal) expr = MK_EXPR(kind::NOT,expr);
+ if(!equal) expr = MK_EXPR(kind::NOT, expr);
}
+ | definedPred[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+ { expr = EXPR_MANAGER->mkExpr(expr, args); }
| definedProp[expr]
-;
+ ;
//%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc.
//%----Note: "defined" means a word starting with one $ and "system" means $$.
: TRUE_TOK { expr = MK_CONST(bool(true)); }
| FALSE_TOK { expr = MK_CONST(bool(false)); }
;
+
+definedPred[CVC4::Expr& expr]
+ : '$less' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LT); }
+ | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); }
+ | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); }
+ | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); }
+ | '$is_rat' // all "real" are actually "rat" in CVC4
+ { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ n = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+ expr = MK_EXPR(CVC4::kind::LAMBDA, n, MK_CONST(bool(true)));
+ }
+ | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); }
+ | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); }
+ ;
+
+definedFun[CVC4::Expr& expr]
+@declarations {
+ bool remainder = false;
+}
+ : '$uminus' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::UMINUS); }
+ | '$sum' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::PLUS); }
+ | '$difference' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MINUS); }
+ | '$product' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MULT); }
+ | '$quotient' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DIVISION_TOTAL); }
+ | ( '$quotient_e' { remainder = false; }
+ | '$remainder_e' { remainder = true; }
+ )
+ { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+ expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+ expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, d, MK_CONST(Rational(0))),
+ MK_EXPR(CVC4::kind::TO_INTEGER, expr),
+ MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
+ if(remainder) {
+ expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+ }
+ expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ }
+ | ( '$quotient_t' { remainder = false; }
+ | '$remainder_t' { remainder = true; }
+ )
+ { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+ expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+ expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, expr, MK_CONST(Rational(0))),
+ MK_EXPR(CVC4::kind::TO_INTEGER, expr),
+ MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
+ if(remainder) {
+ expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+ }
+ expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ }
+ | ( '$quotient_f' { remainder = false; }
+ | '$remainder_f' { remainder = true; }
+ )
+ { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+ expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+ expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr);
+ if(remainder) {
+ expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+ }
+ expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ }
+ | '$floor' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); }
+ | '$ceiling'
+ { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+ expr = MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n)));
+ expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ }
+ | '$truncate'
+ { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+ expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, n, MK_CONST(Rational(0))),
+ MK_EXPR(CVC4::kind::TO_INTEGER, n),
+ MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n))));
+ expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ }
+ | '$round'
+ { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+ Expr decPart = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::TO_INTEGER, n));
+ expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::LT, decPart, MK_CONST(Rational(1, 2))),
+ // if decPart < 0.5, round down
+ MK_EXPR(CVC4::kind::TO_INTEGER, n),
+ MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GT, decPart, MK_CONST(Rational(1, 2))),
+ // if decPart > 0.5, round up
+ MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, n, MK_CONST(Rational(1)))),
+ // if decPart == 0.5, round to nearest even integer:
+ // result is: to_int(n/2 + .5) * 2
+ MK_EXPR(CVC4::kind::MULT, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, MK_CONST(Rational(2))), MK_CONST(Rational(1, 2)))), MK_CONST(Rational(2)))));
+ expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ }
+ | '$to_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); }
+ | '$to_rat' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); }
+ | '$to_real' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); }
+ ;
+
//%----Pure CNF should not use $true or $false in problems, and use $false only
//%----at the roots of a refutation.
-equalOp[bool & equal]
- : EQUAL_TOK {equal = true;}
- | DISEQUAL_TOK {equal = false;}
+equalOp[bool& equal]
+ : EQUAL_TOK { equal = true; }
+ | DISEQUAL_TOK { equal = false; }
;
term[CVC4::Expr& expr]
- : functionTerm[expr]
+ : functionTerm[expr]
+ | conditionalTerm[expr]
| simpleTerm[expr]
-// | conditionalTerm
-// | let_term
+ | letTerm[expr]
+ ;
+
+letTerm[CVC4::Expr& expr]
+@declarations {
+ CVC4::Expr lhs, rhs;
+}
+ : '$let_ft' LPAREN_TOK { PARSER_STATE->pushScope(); }
+ tffLetFormulaDefn[lhs, rhs] COMMA_TOK
+ term[expr]
+ { PARSER_STATE->popScope();
+ expr = expr.substitute(lhs, rhs);
+ }
+ RPAREN_TOK
+ | '$let_tt' LPAREN_TOK { PARSER_STATE->pushScope(); }
+ tffLetTermDefn[lhs, rhs] COMMA_TOK
+ term[expr]
+ { PARSER_STATE->popScope();
+ expr = expr.substitute(lhs, rhs);
+ }
+ RPAREN_TOK
;
/* Not an application */
simpleTerm[CVC4::Expr& expr]
: variable[expr]
| NUMBER { expr = PARSER_STATE->d_tmp_expr; }
- | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(
- AntlrInput::tokenText($DISTINCT_OBJECT)); }
-;
+ | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); }
+ ;
functionTerm[CVC4::Expr& expr]
- : plainTerm[expr] // | <defined_term> | <system_term>
+@declarations {
+ std::vector<CVC4::Expr> args;
+}
+ : plainTerm[expr]
+ | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+ { expr = EXPR_MANAGER->mkExpr(expr, args); }
+// | <system_term>
+ ;
+
+conditionalTerm[CVC4::Expr& expr]
+@declarations {
+ CVC4::Expr expr2, expr3;
+}
+ : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK
+ { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, expr2, expr3); }
;
plainTerm[CVC4::Expr& expr]
-@declarations{
+@declarations {
std::string name;
std::vector<Expr> args;
}
}
;
-arguments[std::vector<CVC4::Expr> & args]
-@declarations{
+arguments[std::vector<CVC4::Expr>& args]
+@declarations {
Expr expr;
}
:
term[expr] { args.push_back(expr); } ( COMMA_TOK term[expr] { args.push_back(expr); } )*
;
-variable[CVC4::Expr & expr]
+variable[CVC4::Expr& expr]
: UPPER_WORD
{
std::string name = AntlrInput::tokenText($UPPER_WORD);
- if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)){
+ if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)) {
expr = PARSER_STATE->getVariable(name);
} else {
expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
/*******/
/* FOF */
-fofFormula[CVC4::Expr & expr] : fofLogicFormula[expr] ;
+fofFormula[CVC4::Expr& expr] : fofLogicFormula[expr] ;
-fofLogicFormula[CVC4::Expr & expr]
-@declarations{
+fofLogicFormula[CVC4::Expr& expr]
+@declarations {
tptp::NonAssoc na;
std::vector< Expr > args;
Expr expr2;
}
: fofUnitaryFormula[expr]
- ( //Non Assoc <=> <~> ~& ~|
+ ( // Non-associative: <=> <~> ~& ~|
( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
- { switch(na){
+ { switch(na) {
case tptp::NA_IFF:
expr = MK_EXPR(kind::IFF,expr,expr2);
break;
}
}
)
- | //And &
+ | // N-ary and &
( { args.push_back(expr); }
( AND_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
- { expr = MK_EXPR(kind::AND,args); }
+ { expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); }
)
- | //Or |
+ | // N-ary or |
( { args.push_back(expr); }
( OR_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
- { expr = MK_EXPR(kind::OR,args); }
+ { expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); }
)
- )?
+ )?
;
-fofUnitaryFormula[CVC4::Expr & expr]
-@declarations{
+fofUnitaryFormula[CVC4::Expr& expr]
+@declarations {
Kind kind;
std::vector< Expr > bv;
}
folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
( bindvariable[expr] { bv.push_back(expr); }
( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
- COLON_TOK fofUnitaryFormula[expr]
- { PARSER_STATE->popScope();
- expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
- } ;
+ COLON_TOK fofUnitaryFormula[expr]
+ { PARSER_STATE->popScope();
+ expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+ }
+ ;
-bindvariable[CVC4::Expr & expr]
+bindvariable[CVC4::Expr& expr]
: UPPER_WORD
- {
- std::string name = AntlrInput::tokenText($UPPER_WORD);
+ { std::string name = AntlrInput::tokenText($UPPER_WORD);
expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
}
- ;
+ ;
-fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na]
+fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc& na]
: IFF_TOK { na = tptp::NA_IFF; }
| REVIFF_TOK { na = tptp::NA_REVIFF; }
| REVOR_TOK { na = tptp::NA_REVOR; }
| REVIMPLIES_TOK { na = tptp::NA_REVIMPLIES; }
;
-folQuantifier[CVC4::Kind & kind]
+folQuantifier[CVC4::Kind& kind]
: BANG_TOK { kind = kind::FORALL; }
| MARK_TOK { kind = kind::EXISTS; }
;
+/*******/
+/* TFF */
+tffFormula[CVC4::Expr& expr] : tffLogicFormula[expr];
+
+tffTypedAtom[CVC4::Command*& cmd]
+@declarations {
+ CVC4::Expr expr;
+ CVC4::Type type;
+ std::string name;
+}
+ : LPAREN_TOK tffTypedAtom[cmd] RPAREN_TOK
+ | nameN[name] COLON_TOK
+ ( '$tType'
+ { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
+ // duplicate declaration is fine, they're compatible
+ cmd = new EmptyCommand("compatible redeclaration of sort " + name);
+ } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
+ // error: cannot be both sort and constant
+ PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a constant; cannot also be a sort");
+ } else {
+ // as yet, it's undeclared
+ Type type = PARSER_STATE->mkSort(name);
+ cmd = new DeclareTypeCommand(name, 0, type);
+ }
+ }
+ | parseType[type]
+ { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
+ // error: cannot be both sort and constant
+ PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a sort");
+ cmd = new EmptyCommand("compatible redeclaration of sort " + name);
+ } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
+ if(type == PARSER_STATE->getVariable(name).getType()) {
+ // duplicate declaration is fine, they're compatible
+ cmd = new EmptyCommand("compatible redeclaration of constant " + name);
+ } else {
+ // error: sorts incompatible
+ PARSER_STATE->parseError("Symbol `" + name + "' declared previously with a different sort");
+ }
+ } else {
+ // as yet, it's undeclared
+ CVC4::Expr expr;
+ if(type.isFunction()) {
+ expr = PARSER_STATE->mkTffFunction(name, type);
+ } else {
+ expr = PARSER_STATE->mkTffVar(name, type);
+ }
+ cmd = new DeclareFunctionCommand(name, expr, type);
+ }
+ }
+ )
+ ;
+
+tffLogicFormula[CVC4::Expr& expr]
+@declarations {
+ tptp::NonAssoc na;
+ std::vector< Expr > args;
+ Expr expr2;
+}
+ : tffUnitaryFormula[expr]
+ ( // Non Assoc <=> <~> ~& ~|
+ ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
+ { switch(na) {
+ case tptp::NA_IFF:
+ expr = MK_EXPR(kind::IFF,expr,expr2);
+ break;
+ case tptp::NA_REVIFF:
+ expr = MK_EXPR(kind::XOR,expr,expr2);
+ break;
+ case tptp::NA_IMPLIES:
+ expr = MK_EXPR(kind::IMPLIES,expr,expr2);
+ break;
+ case tptp::NA_REVIMPLIES:
+ expr = MK_EXPR(kind::IMPLIES,expr2,expr);
+ break;
+ case tptp::NA_REVOR:
+ expr = MK_EXPR(kind::NOT,MK_EXPR(kind::OR,expr,expr2));
+ break;
+ case tptp::NA_REVAND:
+ expr = MK_EXPR(kind::NOT,MK_EXPR(kind::AND,expr,expr2));
+ break;
+ }
+ }
+ )
+ | // And &
+ ( { args.push_back(expr); }
+ ( AND_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
+ { expr = MK_EXPR(kind::AND,args); }
+ )
+ | // Or |
+ ( { args.push_back(expr); }
+ ( OR_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
+ { expr = MK_EXPR(kind::OR,args); }
+ )
+ )?
+ ;
+
+tffUnitaryFormula[CVC4::Expr& expr]
+@declarations {
+ Kind kind;
+ std::vector< Expr > bv;
+ Expr lhs, rhs;
+}
+ : atomicFormula[expr]
+ | LPAREN_TOK tffLogicFormula[expr] RPAREN_TOK
+ | NOT_TOK tffUnitaryFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
+ | // Quantified
+ folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
+ ( tffbindvariable[expr] { bv.push_back(expr); }
+ ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
+ COLON_TOK tffUnitaryFormula[expr]
+ { PARSER_STATE->popScope();
+ expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+ }
+ | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK
+ { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, lhs, rhs); }
+ | '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); }
+ tffLetTermDefn[lhs, rhs] COMMA_TOK
+ tffFormula[expr]
+ { PARSER_STATE->popScope();
+ expr = expr.substitute(lhs, rhs);
+ }
+ RPAREN_TOK
+ | '$let_ff' LPAREN_TOK { PARSER_STATE->pushScope(); }
+ tffLetFormulaDefn[lhs, rhs] COMMA_TOK
+ tffFormula[expr]
+ { PARSER_STATE->popScope();
+ expr = expr.substitute(lhs, rhs);
+ }
+ RPAREN_TOK
+ ;
+
+tffLetTermDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+@declarations {
+ std::vector<CVC4::Expr> bvlist;
+}
+ : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
+ tffLetTermBinding[bvlist, lhs, rhs]
+ ;
+
+tffLetTermBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+ : term[lhs] EQUAL_TOK term[rhs]
+ { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
+ rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
+ lhs = lhs.getOperator();
+ }
+ | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
+ ;
+
+tffLetFormulaDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+@declarations {
+ std::vector<CVC4::Expr> bvlist;
+}
+ : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
+ tffLetFormulaBinding[bvlist, lhs, rhs]
+ ;
+
+tffLetFormulaBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+ : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs]
+ { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
+ rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
+ lhs = lhs.getOperator();
+ }
+ | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
+ ;
+
+tffbindvariable[CVC4::Expr& expr]
+@declarations {
+ CVC4::Type type = PARSER_STATE->d_unsorted;
+}
+ : UPPER_WORD
+ ( COLON_TOK parseType[type] )?
+ { std::string name = AntlrInput::tokenText($UPPER_WORD);
+ expr = PARSER_STATE->mkBoundVar(name, type);
+ }
+ ;
+
+// bvlist is accumulative; it can already contain elements
+// on the way in, which are left undisturbed
+tffVariableList[std::vector<CVC4::Expr>& bvlist]
+@declarations {
+ CVC4::Expr e;
+}
+ : tffbindvariable[e] { bvlist.push_back(e); }
+ ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )*
+ ;
+
+parseType[CVC4::Type& type]
+@declarations {
+ std::vector<CVC4::Type> v;
+}
+ : simpleType[type]
+ | ( simpleType[type] { v.push_back(type); }
+ | LPAREN_TOK simpleType[type] { v.push_back(type); }
+ ( TIMES_TOK simpleType[type] { v.push_back(type); } )+
+ RPAREN_TOK
+ )
+ GREATER_TOK simpleType[type]
+ { v.push_back(type);
+ type = EXPR_MANAGER->mkFunctionType(v);
+ }
+ ;
+
+// non-function types
+simpleType[CVC4::Type& type]
+ : DEFINED_SYMBOL
+ { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL);
+ if(s == "\$i") type = PARSER_STATE->d_unsorted;
+ else if(s == "\$o") type = EXPR_MANAGER->booleanType();
+ else if(s == "\$int") type = EXPR_MANAGER->integerType();
+ else if(s == "\$rat") type = EXPR_MANAGER->realType();
+ else if(s == "\$real") type = EXPR_MANAGER->realType();
+ else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here");
+ else PARSER_STATE->parseError("unknown defined type `" + s + "'");
+ }
+ | LOWER_WORD
+ { type = PARSER_STATE->getSort(AntlrInput::tokenText($LOWER_WORD)); }
+ ;
+
/***********************************************/
/* Anything well parenthesis */
| FOF_TOK
| THF_TOK
| TFF_TOK
+ | TYPE_TOK
| INCLUDE_TOK
| DISTINCT_OBJECT
| UPPER_WORD
RBRACK_TOK : ']';
COLON_TOK : ':';
+GREATER_TOK : '>';
+
//operator
OR_TOK : '|';
NOT_TOK : '~';
FOF_TOK : 'fof';
THF_TOK : 'thf';
TFF_TOK : 'tff';
+TYPE_TOK : 'type';
INCLUDE_TOK : 'include';
//Other defined symbols, must be defined after all the other
LOWER_WORD : LOWER_ALPHA ALPHA_NUMERIC*;
/* filename */
-unquotedFileName[std::string & name] /* Beware fileName identifier is used by the backend ... */
+unquotedFileName[std::string& name] /* Beware fileName identifier is used by the backend ... */
: (s=LOWER_WORD_SINGLE_QUOTED | s=SINGLE_QUOTED)
{ name = AntlrInput::tokenText($s);
name = name.substr(1, name.size() - 2 );
};
/* axiom name */
-nameN[std::string & name]
+nameN[std::string& name]
: atomicWord[name]
| NUMBER { name = AntlrInput::tokenText($NUMBER); }
;
/* atomic word everything (fof, cnf, thf, tff, include must not be keyword at this position ) */
-atomicWord[std::string & name]
+atomicWord[std::string& name]
: FOF_TOK { name = "fof"; }
| CNF_TOK { name = "cnf"; }
| THF_TOK { name = "thf"; }
| TFF_TOK { name = "tff"; }
+ | TYPE_TOK { name = "type"; }
| INCLUDE_TOK { name = "include"; }
| LOWER_WORD { name = AntlrInput::tokenText($LOWER_WORD); }
- | LOWER_WORD_SINGLE_QUOTED //the lower word single quoted are considered without quote
- {
- /* strip off the quotes */
- name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED,1,
+ | LOWER_WORD_SINGLE_QUOTED // the lower word single quoted are considered without quote
+ { /* strip off the quotes */
+ name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED, 1 ,
($LOWER_WORD_SINGLE_QUOTED->stop - $LOWER_WORD_SINGLE_QUOTED->start) - 1);
}
| SINGLE_QUOTED {name = AntlrInput::tokenText($SINGLE_QUOTED); }; //for the others the quote remains
/* Rational */
fragment DOT : '.';
-fragment EXPONENT : 'E'|'e';
+fragment EXPONENT : 'E' | 'e';
fragment SLASH : '/';
fragment DECIMAL : NUMERIC+;
-/* Currently we put all in the rationnal type */
-fragment SIGN[bool & pos] : PLUS_TOK | MINUS_TOK { pos = false; } ;
-
+/* Currently we put all in the rational type */
+fragment SIGN[bool& pos]
+ : PLUS_TOK { pos = true; }
+ | MINUS_TOK { pos = false; }
+ ;
NUMBER
-@declarations{
+@declarations {
bool pos = true;
bool posE = true;
}
- :
- ( SIGN[pos]? num=DECIMAL
- {
- Integer i (AntlrInput::tokenText($num));
- Rational r = ( pos ? i : -i );
- PARSER_STATE->d_tmp_expr = MK_CONST(r);
- }
- | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
- {
- std::string snum = AntlrInput::tokenText($num);
+ : ( SIGN[pos]? num=DECIMAL
+ { Integer i(AntlrInput::tokenText($num));
+ Rational r = pos ? i : -i;
+ PARSER_STATE->d_tmp_expr = MK_CONST(r);
+ }
+ | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
+ { std::string snum = AntlrInput::tokenText($num);
std::string sden = AntlrInput::tokenText($den);
/* compute the numerator */
- Integer inum( snum + sden );
+ Integer inum(snum + sden);
// The sign
- inum = pos ? inum : - inum;
+ inum = pos ? inum : -inum;
// The exponent
size_t exp = ($e == NULL ? 0 : AntlrInput::tokenToUnsigned($e));
// Decimal part
/* multiply it by 10 raised to the exponent reduced by the
* number of decimal place in den (dec) */
Rational r;
- if( !posE ) r = Rational(inum, Integer(10).pow(exp + dec));
- else if( exp == dec ) r = Rational(inum);
- else if( exp > dec ) r = Rational(inum * Integer(10).pow(exp - dec));
+ if(!posE) r = Rational(inum, Integer(10).pow(exp + dec));
+ else if(exp == dec) r = Rational(inum);
+ else if(exp > dec) r = Rational(inum * Integer(10).pow(exp - dec));
else r = Rational(inum, Integer(10).pow(dec - exp));
- PARSER_STATE->d_tmp_expr = MK_CONST( r );
+ PARSER_STATE->d_tmp_expr = MK_CONST(r);
+ }
+ | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
+ { Integer inum(AntlrInput::tokenText($num));
+ Integer iden(AntlrInput::tokenText($den));
+ PARSER_STATE->d_tmp_expr = MK_CONST(Rational(pos ? inum : -inum, iden));
+ }
+ )
+ { if(PARSER_STATE->cnf || PARSER_STATE->fof) {
+ // We're in an unsorted context, so put a conversion around it
+ PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
}
- | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
- {
- Integer inum(AntlrInput::tokenText($num));
- Integer iden(AntlrInput::tokenText($den));
- PARSER_STATE->d_tmp_expr = MK_CONST(
- Rational(pos ? inum : -inum, iden));
- }
- ) {
- //Put a convertion around it
- PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
}
;
-
/**
* Matches the comments and ignores them
*/
| '/*' ( options {greedy=false;} : . )* '*/' { SKIP(); } //comment block
;
-
-
/* 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");
+ 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;
+// 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 {
+ if(home != NULL) {
d_tptpDir = home;
- //add trailing "/"
- if( d_tptpDir[d_tptpDir.size() - 1] != '/'){
- d_tptpDir.append("/");
- }
+ d_tptpDir.append("/TPTP/");
}
- d_hasConjecture = false;
+ } else {
+ d_tptpDir = home;
+ //add trailing "/"
+ if(d_tptpDir[d_tptpDir.size() - 1] != '/') {
+ d_tptpDir.append("/");
+ }
+ }
+ d_hasConjecture = false;
}
void Tptp::addTheory(Theory theory) {
/* 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){
+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.
#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 ) {
+ if(in == NULL) {
Debug("parser") << "Can't open " << fileName << std::endl;
return false;
}
return true;
}
+/* overridden popCharStream for the lexer - necessary if we had symbol
+ * filtering in file inclusion.
+void Tptp::myPopCharStream(pANTLR3_LEXER lexer) {
+ ((Tptp*)lexer->super)->d_oldPopCharStream(lexer);
+ ((Tptp*)lexer->super)->popScope();
+}
+*/
-void Tptp::includeFile(std::string fileName){
+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();
+
+ // set up popCharStream - would be necessary for handling symbol
+ // filtering in inclusions
+ /*
+ if(d_oldPopCharStream == NULL) {
+ d_oldPopCharStream = lexer->popCharStream;
+ lexer->popCharStream = myPopCharStream;
+ }
+ */
+
+ // 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>"){
+ if(inputName != "<stdin>") {
// TODO: Use dirname ot Boost::filesystem?
size_t pos = inputName.rfind('/');
- if( pos != std::string::npos){
+ if(pos != std::string::npos) {
currentDirFileName = std::string(inputName, 0, pos + 1);
}
currentDirFileName.append(fileName);
- if( newInputStream(currentDirFileName,lexer) ){
+ if(newInputStream(currentDirFileName,lexer)) {
return;
}
} else {
currentDirFileName = "<unknown current directory for stdin>";
}
- if( d_tptpDir.empty() ){
+ 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) ){
+ if(! newInputStream(tptpDirFileName,lexer)) {
parseError("Couldn't open included file: " + fileName
+ " at " + currentDirFileName + " or " + tptpDirFileName);
}
}
+void Tptp::checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula) {
+ if(lhs.getKind() != CVC4::kind::APPLY_UF) {
+ parseError("malformed let: LHS must be a flat function application");
+ }
+ std::vector<CVC4::Expr> v = lhs.getChildren();
+ if(formula && !lhs.getType().isBoolean()) {
+ parseError("malformed let: LHS must be formula");
+ }
+ for(size_t i = 0; i < v.size(); ++i) {
+ if(v[i].hasOperator()) {
+ parseError("malformed let: LHS must be flat, illegal child: " + v[i].toString());
+ }
+ }
+ std::sort(v.begin(), v.end());
+ std::sort(bvlist.begin(), bvlist.end());
+ // ensure all let-bound variables appear on the LHS, and appear only once
+ for(size_t i = 0; i < bvlist.size(); ++i) {
+ std::vector<CVC4::Expr>::const_iterator found = std::lower_bound(v.begin(), v.end(), bvlist[i]);
+ if(found == v.end() || *found != bvlist[i]) {
+ parseError("malformed let: LHS must make use of all quantified variables, missing `" + bvlist[i].toString() + "'");
+ }
+ std::vector<CVC4::Expr>::const_iterator found2 = found + 1;
+ if(found2 != v.end() && *found2 == *found) {
+ parseError("malformed let: LHS cannot use same bound variable twice: " + (*found).toString());
+ }
+ }
+}
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
#include <ext/hash_set>
#include <cassert>
#include "parser/options.h"
+#include "parser/antlr_input.h"
namespace CVC4 {
std::hash_set<Expr, ExprHashFunction> d_r_converted;
std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
- //TPTP directory where to find includes
+ // TPTP directory where to find includes;
// empty if none could be determined
std::string d_tptpDir;
- //hack to make output SZS ontology-compliant
+ // hack to make output SZS ontology-compliant
bool d_hasConjecture;
- // hack for szs compliance
- bool d_szsCompliant;
+
+ static void myPopCharStream(pANTLR3_LEXER lexer);
+ void (*d_oldPopCharStream)(pANTLR3_LEXER);
public:
- bool cnf; //in a cnf formula
- void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); };
- std::vector< Expr > getFreeVar(){
+ bool cnf; // in a cnf formula
+ bool fof; // in an fof formula
+
+ void addFreeVar(Expr var) {
+ assert(cnf);
+ d_freeVar.push_back(var);
+ }
+ std::vector< Expr > getFreeVar() {
assert(cnf);
std::vector< Expr > r;
r.swap(d_freeVar);
return r;
}
- inline Expr convertRatToUnsorted(Expr expr){
+ inline Expr convertRatToUnsorted(Expr expr) {
ExprManager * em = getExprManager();
// Create the conversion function If they doesn't exists
- if(d_rtu_op.isNull()){
+ if(d_rtu_op.isNull()) {
Type t;
- //Conversion from rational to unsorted
+ // Conversion from rational to unsorted
t = em->mkFunctionType(em->realType(), d_unsorted);
d_rtu_op = em->mkVar("$$rtu",t);
preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
- //Conversion from unsorted to rational
+ // Conversion from unsorted to rational
t = em->mkFunctionType(d_unsorted, em->realType());
d_utr_op = em->mkVar("$$utr",t);
- preemptCommand(new DeclareFunctionCommand("$$utur", d_utr_op, t));
+ 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
Expr ret = em->mkExpr(kind::APPLY_UF,d_rtu_op,expr);
- if ( d_r_converted.find(expr) == d_r_converted.end() ){
+ if(d_r_converted.find(expr) == d_r_converted.end()) {
d_r_converted.insert(expr);
- Expr eq = em->mkExpr(kind::EQUAL,expr,
- em->mkExpr(kind::APPLY_UF,d_utr_op,ret));
+ Expr eq = em->mkExpr(kind::EQUAL, expr,
+ em->mkExpr(kind::APPLY_UF, d_utr_op, ret));
preemptCommand(new AssertCommand(eq));
- };
+ }
return ret;
}
public:
- //TPTP (CNF and FOF) is unsorted so we define this common type
+ // CNF and FOF are unsorted so we define this common type.
+ // This is also the Type of $i in TFF.
Type d_unsorted;
enum Theory {
THEORY_CORE,
- };
+ };/* enum Theory */
enum FormulaRole {
FR_AXIOM,
FR_FI_FUNCTORS,
FR_FI_PREDICATES,
FR_TYPE,
- };
+ };/* enum FormulaRole */
+ bool hasConjecture() const { return d_hasConjecture; }
protected:
Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
*/
void addTheory(Theory theory);
- inline void makeApplication(Expr & expr, std::string & name,
- std::vector<Expr> & args, bool term);
+ inline void makeApplication(Expr& expr, std::string& name,
+ std::vector<Expr>& args, bool term);
+
+ inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf);
+
+ inline Expr mkTffVar(std::string& name, const Type& type) {
+ std::string orig = name;
+ std::stringstream ss;
+ ss << name << "_0";
+ name = ss.str();
+ Expr var = mkVar(name, type);
+ defineFunction(orig, var);
+ return var;
+ }
- inline Command* makeCommand(FormulaRole fr, Expr & expr);
+ inline Expr mkTffFunction(std::string& name, const FunctionType& type) {
+ std::string orig = name;
+ std::stringstream ss;
+ ss << name << "_" << type.getArity();
+ name = ss.str();
+ Expr fun = mkFunction(name, type);
+ defineFunction(orig, fun);
+ return fun;
+ }
/** Ugly hack because I don't know how to return an expression from a
token */
is reused */
void includeFile(std::string fileName);
+ /** Check a TPTP let binding for well-formedness. */
+ void checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula);
+
private:
void addArithmeticOperators();
};/* class Tptp */
-inline void Tptp::makeApplication(Expr & expr, std::string & name,
- std::vector<Expr> & args, bool term){
+inline void Tptp::makeApplication(Expr& expr, std::string& name,
+ std::vector<Expr>& args, bool term) {
// We distinguish the symbols according to their arities
std::stringstream ss;
ss << name << "_" << args.size();
name = ss.str();
- if(args.empty()){ // Its a constant
- if(isDeclared(name)){ //already appeared
+ if(args.empty()) { // Its a constant
+ if(isDeclared(name)) { // already appeared
expr = getVariable(name);
} else {
Type t = term ? d_unsorted : getExprManager()->booleanType();
- expr = mkVar(name,t,true); //levelZero
+ expr = mkVar(name, t, true); // levelZero
preemptCommand(new DeclareFunctionCommand(name, expr, t));
}
} else { // Its an application
- if(isDeclared(name)){ //already appeared
+ if(isDeclared(name)) { // already appeared
expr = getVariable(name);
} else {
std::vector<Type> sorts(args.size(), d_unsorted);
Type t = term ? d_unsorted : getExprManager()->booleanType();
t = getExprManager()->mkFunctionType(sorts, t);
- expr = mkVar(name,t,true); //levelZero
+ expr = mkVar(name, t, true); // levelZero
preemptCommand(new DeclareFunctionCommand(name, expr, 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].getType().isReal() && FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) {
+ args[i] = convertRatToUnsorted(args[i]);
+ }
+ }
expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args);
}
-};
+}
-inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){
- //hack for SZS ontology compliance
- if(d_szsCompliant && (fr==FR_NEGATED_CONJECTURE || fr==FR_CONJECTURE)){
- if( !d_hasConjecture ){
- d_hasConjecture = true;
- std::cout << "conjecture-";
- }
+inline Command* Tptp::makeCommand(FormulaRole fr, Expr& 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;
}
- switch(fr){
+ switch(fr) {
case FR_AXIOM:
case FR_HYPOTHESIS:
case FR_DEFINITION:
namespace CVC4 {
namespace parser {
-/* Use lookahead=1 */
+/* Use lookahead=2 */
TptpInput::TptpInput(AntlrInputStream& inputStream) :
- AntlrInput(inputStream, 1) {
+ AntlrInput(inputStream, 2) {
pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
assert( input != NULL );
smt2/smt2_printer.h \
smt2/smt2_printer.cpp \
cvc/cvc_printer.h \
- cvc/cvc_printer.cpp
+ cvc/cvc_printer.cpp \
+ tptp/tptp_printer.h \
+ tptp/tptp_printer.cpp
EXTRA_DIST = \
options_handlers.h
#include "printer/smt1/smt1_printer.h"
#include "printer/smt2/smt2_printer.h"
+#include "printer/tptp/tptp_printer.h"
#include "printer/cvc/cvc_printer.h"
#include "printer/ast/ast_printer.h"
case LANG_SMTLIB_V2:
return new printer::smt2::Smt2Printer();
- case LANG_TPTP: //TODO the printer
- return new printer::smt2::Smt2Printer();
+ case LANG_TPTP:
+ return new printer::tptp::TptpPrinter();
case LANG_CVC4:
return new printer::cvc::CvcPrinter();
/** write model response to command */
virtual void toStream(std::ostream& out, const Model& m, const Command* c) const throw() = 0;
+ /** write model response to command using another language printer */
+ void toStreamUsing(OutputLanguage lang, std::ostream& out, const Model& m, const Command* c) const throw() {
+ getPrinter(lang)->toStream(out, m, c);
+ }
+
public:
/** Get the Printer for a given OutputLanguage */
static Printer* getPrinter(OutputLanguage lang) throw() {
}
void Smt2Printer::toStream(std::ostream& out, const Result& r) const throw() {
- if (r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
+ if(r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
out << "unknown";
} else {
Printer::toStream(out, r);
--- /dev/null
+/********************* */
+/*! \file tptp_printer.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the TPTP output language
+ **
+ ** The pretty-printer interface for the TPTP output language.
+ **/
+
+#include "printer/tptp/tptp_printer.h"
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "util/language.h" // for LANG_AST
+#include "expr/node_manager.h" // for VarNameAttr
+#include "expr/command.h"
+
+#include <iostream>
+#include <vector>
+#include <string>
+#include <typeinfo>
+
+using namespace std;
+
+namespace CVC4 {
+namespace printer {
+namespace tptp {
+
+void TptpPrinter::toStream(std::ostream& out, TNode n,
+ int toDepth, bool types, size_t dag) const throw() {
+ n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const Command* c,
+ int toDepth, bool types, size_t dag) const throw() {
+ c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+ s->toStream(out, language::output::LANG_SMTLIB_V2);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+ Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+}/* TptpPrinter::toStream() */
+
+void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
+ out << "% SZS output start FiniteModel for " << m.getInputName() << endl;
+ for(size_t i = 0; i < m.getNumCommands(); ++i) {
+ this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2, out, m, m.getCommand(i));
+ }
+ out << "% SZS output end FiniteModel for " << m.getInputName() << endl;
+}
+
+void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c) const throw() {
+ // shouldn't be called; only the non-Command* version above should be
+ Unreachable();
+}
+
+void TptpPrinter::toStream(std::ostream& out, const Result& r) const throw() {
+ out << "% SZS status ";
+ if(r.isSat() == Result::SAT) {
+ out << "Satisfiable";
+ } else if(r.isSat() == Result::UNSAT) {
+ out << "Unsatisfiable";
+ } else if(r.isValid() == Result::VALID) {
+ out << "Theorem";
+ } else if(r.isValid() == Result::INVALID) {
+ out << "CounterSatisfiable";
+ } else {
+ out << "GaveUp";
+ }
+ out << " for " << r.getInputName();
+}
+
+}/* CVC4::printer::tptp namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file tptp_printer.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The pretty-printer interface for the TPTP output language
+ **
+ ** The pretty-printer interface for the TPTP output language.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PRINTER__TPTP_PRINTER_H
+#define __CVC4__PRINTER__TPTP_PRINTER_H
+
+#include <iostream>
+
+#include "printer/printer.h"
+
+namespace CVC4 {
+namespace printer {
+namespace tptp {
+
+class TptpPrinter : public CVC4::Printer {
+ void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
+public:
+ using CVC4::Printer::toStream;
+ void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
+ void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
+ void toStream(std::ostream& out, const CommandStatus* s) const throw();
+ void toStream(std::ostream& out, const SExpr& sexpr) const throw();
+ void toStream(std::ostream& out, const Model& m) const throw();
+ void toStream(std::ostream& out, const Result& r) const throw();
+};/* class TptpPrinter */
+
+}/* CVC4::printer::tptp namespace */
+}/* CVC4::printer namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PRINTER__TPTP_PRINTER_H */
}
// Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
- if(key == "name" ||
- key == "source" ||
+ if(key == "source" ||
key == "category" ||
key == "difficulty" ||
key == "notes") {
// ignore these
return;
+ } else if(key == "name") {
+ d_filename = value.getValue();
+ return;
} else if(key == "smt-lib-version") {
if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
(value.isRational() && value.getRationalValue() == Rational(2)) ||
throw OptionException("argument to (set-info :status ..) must be "
"`sat' or `unsat' or `unknown'");
}
- d_status = Result(s);
+ d_status = Result(s, d_filename);
return;
}
throw UnrecognizedOptionException();
if(d_timeBudgetCumulative != 0) {
millis = getTimeRemaining();
if(millis == 0) {
- return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT);
+ return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT, d_filename);
}
}
if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
if(d_resourceBudgetCumulative != 0) {
resource = getResourceRemaining();
if(resource == 0) {
- return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT);
+ return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT, d_filename);
}
}
if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
<< ", conflicts " << d_cumulativeResourceUsed << endl;
- return result;
+ return Result(result, d_filename);
}
Result SmtEngine::quickCheck() {
Assert(d_fullyInited);
Trace("smt") << "SMT quickCheck()" << endl;
- return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK);
+ return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK, d_filename);
}
"Cannot get model when produce-models options is off.";
throw ModalException(msg);
}
- return d_theoryEngine->getModel();
+ TheoryModel* m = d_theoryEngine->getModel();
+ m->d_inputName = d_filename;
+ return m;
}
void SmtEngine::checkModel(bool hardFailure) {
*/
Result d_status;
+ /**
+ * The name of the input (if any).
+ */
+ std::string d_filename;
+
/**
* A private utility class to SmtEngine.
*/
operator LAMBDA 2 "lambda"
-parameterized CHAIN BUILTIN 2: "chain operator"
+parameterized CHAIN CHAIN_OP 2: "chained operator"
+constant CHAIN_OP \
+ ::CVC4::Chain \
+ ::CVC4::ChainHashFunction \
+ "util/chain.h" \
+ "the chained operator"
constant TYPE_CONSTANT \
::CVC4::TypeConstant \
typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
+typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
constant SUBTYPE_TYPE \
::CVC4::Predicate \
**/
#include "theory/builtin/theory_builtin_rewriter.h"
+#include "util/chain.h"
using namespace std;
Assert(in.getKind() == kind::CHAIN);
- Kind chainedOp = in.getOperator().getConst<Kind>();
+ Kind chainedOp = in.getOperator().getConst<Chain>().getOperator();
if(in.getNumChildren() == 2) {
// if this is the case exactly 1 pair will be generated so the
}
};/* class ChainTypeRule */
+class ChainedOperatorTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+ Assert(n.getKind() == kind::CHAIN_OP);
+ return nodeManager->getType(nodeManager->operatorOf(n.getConst<Chain>().getOperator()), check);
+ }
+};/* class ChainedOperatorTypeRule */
+
class SortProperties {
public:
inline static bool isWellFounded(TypeNode type) {
ite_removal.h \
ite_removal.cpp \
node_visitor.h \
+ chain.h \
index.h \
uninterpreted_constant.h \
uninterpreted_constant.cpp \
rational.i \
hash.i \
predicate.i \
- uninterpreted_constant.i
+ uninterpreted_constant.i \
+ chain.i
DISTCLEANFILES = \
integer.h.tmp \
#include <vector>
#include <algorithm>
+#include "expr/expr_manager_scope.h"
#include "expr/node.h"
#include "util/cvc4_assert.h"
* @param e the Expr to negate (cannot be the null Expr)
*/
static Expr negate(Expr e) throw(AssertionException) {
+ ExprManagerScope ems(e);
return negate(Node::fromExpr(e)).toExpr();
}
--- /dev/null
+/********************* */
+/*! \file chain.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CHAIN_H
+#define __CVC4__CHAIN_H
+
+#include "expr/kind.h"
+#include <iostream>
+
+namespace CVC4 {
+
+/** A class to represent a chained, built-in operator. */
+class Chain {
+ Kind d_kind;
+public:
+ explicit Chain(Kind k) : d_kind(k) { }
+ bool operator==(const Chain& ch) const { return d_kind == ch.d_kind; }
+ bool operator!=(const Chain& ch) const { return d_kind != ch.d_kind; }
+ Kind getOperator() const { return d_kind; }
+};/* class Chain */
+
+inline std::ostream& operator<<(std::ostream& out, const Chain& ch) {
+ return out << ch.getOperator();
+}
+
+struct ChainHashFunction {
+ size_t operator()(const Chain& ch) const {
+ return kind::KindHashFunction()(ch.getOperator());
+ }
+};/* struct ChainHashFunction */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CHAIN_H */
--- /dev/null
+%{
+#include "util/chain.h"
+%}
+
+%rename(equals) CVC4::Chain::operator==(const Chain&) const;
+%ignore CVC4::Chain::operator!=(const Chain&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Chain&);
+
+%rename(apply) CVC4::ChainHashFunction::operator()(const CVC4::Chain&) const;
+
+%include "util/chain.h"
namespace CVC4 {
-Result::Result(const std::string& instr) :
+Result::Result(const std::string& instr, std::string inputName) :
d_sat(SAT_UNKNOWN),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
string s = instr;
transform(s.begin(), s.end(), s.begin(), ::tolower);
if(s == "sat" || s == "satisfiable") {
switch(d_validity) {
case INVALID:
- return Result(SAT);
+ return Result(SAT, d_inputName);
case VALID:
- return Result(UNSAT);
+ return Result(UNSAT, d_inputName);
case VALIDITY_UNKNOWN:
- return Result(SAT_UNKNOWN, d_unknownExplanation);
+ return Result(SAT_UNKNOWN, d_unknownExplanation, d_inputName);
default:
Unhandled(d_validity);
}
// TYPE_NONE
- return Result(SAT_UNKNOWN, NO_STATUS);
+ return Result(SAT_UNKNOWN, NO_STATUS, d_inputName);
}
Result Result::asValidityResult() const throw() {
switch(d_sat) {
case SAT:
- return Result(INVALID);
+ return Result(INVALID, d_inputName);
case UNSAT:
- return Result(VALID);
+ return Result(VALID, d_inputName);
case SAT_UNKNOWN:
- return Result(VALIDITY_UNKNOWN, d_unknownExplanation);
+ return Result(VALIDITY_UNKNOWN, d_unknownExplanation, d_inputName);
default:
Unhandled(d_sat);
}
// TYPE_NONE
- return Result(VALIDITY_UNKNOWN, NO_STATUS);
+ return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName);
}
string Result::toString() const {
enum Validity d_validity;
enum Type d_which;
enum UnknownExplanation d_unknownExplanation;
+ std::string d_inputName;
public:
- Result() :
+ Result(std::string inputName = "") :
d_sat(SAT_UNKNOWN),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_NONE),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
}
- Result(enum Sat s) :
+ Result(enum Sat s, std::string inputName = "") :
d_sat(s),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_SAT),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
CheckArgument(s != SAT_UNKNOWN,
"Must provide a reason for satisfiability being unknown");
}
- Result(enum Validity v) :
+ Result(enum Validity v, std::string inputName = "") :
d_sat(SAT_UNKNOWN),
d_validity(v),
d_which(TYPE_VALIDITY),
- d_unknownExplanation(UNKNOWN_REASON) {
+ d_unknownExplanation(UNKNOWN_REASON),
+ d_inputName(inputName) {
CheckArgument(v != VALIDITY_UNKNOWN,
"Must provide a reason for validity being unknown");
}
- Result(enum Sat s, enum UnknownExplanation unknownExplanation) :
+ Result(enum Sat s, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
d_sat(s),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_SAT),
- d_unknownExplanation(unknownExplanation) {
+ d_unknownExplanation(unknownExplanation),
+ d_inputName(inputName) {
CheckArgument(s == SAT_UNKNOWN,
"improper use of unknown-result constructor");
}
- Result(enum Validity v, enum UnknownExplanation unknownExplanation) :
+ Result(enum Validity v, enum UnknownExplanation unknownExplanation, std::string inputName = "") :
d_sat(SAT_UNKNOWN),
d_validity(v),
d_which(TYPE_VALIDITY),
- d_unknownExplanation(unknownExplanation) {
+ d_unknownExplanation(unknownExplanation),
+ d_inputName(inputName) {
CheckArgument(v == VALIDITY_UNKNOWN,
"improper use of unknown-result constructor");
}
- Result(const std::string& s);
+ Result(const std::string& s, std::string inputName = "");
+
+ Result(const Result& r, std::string inputName) {
+ *this = r;
+ d_inputName = inputName;
+ }
enum Sat isSat() const {
return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN;
std::string toString() const;
+ std::string getInputName() const { return d_inputName; }
+
};/* class Result */
inline bool Result::operator!=(const Result& r) const throw() {
class Model {
friend std::ostream& operator<<(std::ostream&, const Model&);
+ friend class SmtEngine;
+
+ /** the input name (file name, etc.) this model is associated to */
+ std::string d_inputName;
protected:
/** The SmtEngine we're associated with */
SmtEngine* getSmtEngine() { return &d_smt; }
/** get the smt engine (as a pointer-to-const) that this model is hooked up to */
const SmtEngine* getSmtEngine() const { return &d_smt; }
+ /** get the input name (file name, etc.) this model is associated to */
+ std::string getInputName() const { return d_inputName; }
public:
/** get value for expression */
regress/regress0/push-pop/boolean \
regress/regress0/precedence \
regress/regress0/preprocess \
+ regress/regress0/tptp \
regress/regress0/unconstrained \
regress/regress0/decision \
regress/regress0/fmf \
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf
-DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf
+DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf
BINARY = cvc4
LOG_COMPILER = @srcdir@/../run_regression
print_lambda.cvc
# Regression tests for TPTP inputs
-TPTP_TESTS = \
- tptp_parser.p \
- tptp_parser2.p \
- tptp_parser3.p \
- tptp_parser4.p \
- tptp_parser5.p \
- tptp_parser6.p \
- tptp_parser7.p \
- tptp_parser8.p \
- tptp_parser9.p \
- tptp_parser10.p
+TPTP_TESTS =
# Regression tests derived from bug reports
BUG_TESTS = \
--- /dev/null
+%------------------------------------------------------------------------------
+% File : ARI086=1 : TPTP v5.5.0. Released v5.0.0.
+% Domain : Arithmetic
+% Problem : Integer: Sum 2 and 2 is 5
+% Version : Especial.
+% English :
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : CounterSatisfiable
+% Rating : 0.00 v5.2.0, 1.00 v5.0.0
+% Syntax : Number of formulae : 1 ( 1 unit; 0 type)
+% Number of atoms : 1 ( 1 equality)
+% Maximal formula depth : 1 ( 1 average)
+% Number of connectives : 0 ( 0 ~; 0 |; 0 &)
+% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
+% ( 0 ~|; 0 ~&)
+% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
+% Number of predicates : 1 ( 0 propositional; 2-2 arity)
+% Number of functors : 3 ( 2 constant; 0-2 arity)
+% Number of variables : 0 ( 0 sgn; 0 !; 0 ?)
+% Maximal term depth : 2 ( 2 average)
+% Arithmetic symbols : 3 ( 0 pred; 1 func; 2 numbers)
+% SPC : TFF_CSA_EQU_ARI
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(anti_sum_2_2_5,conjecture,
+ ( $sum(2,2) = 5 )).
+%------------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : BOO004-0 : TPTP v5.5.0. Released v1.0.0.
+% Domain : Boolean Algebra
+% Axioms : Boolean algebra (equality) axioms
+% Version : [Ver94] (equality) axioms.
+% English :
+
+% Refs : [Ver94] Veroff (1994), Problem Set
+% Source : [Ver94]
+% Names :
+
+% Status : Satisfiable
+% Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 0 RR)
+% Number of atoms : 8 ( 8 equality)
+% Maximal clause size : 1 ( 1 average)
+% Number of predicates : 1 ( 0 propositional; 2-2 arity)
+% Number of functors : 5 ( 2 constant; 0-2 arity)
+% Number of variables : 14 ( 0 singleton)
+% Maximal term depth : 3 ( 2 average)
+% SPC :
+
+% Comments :
+%--------------------------------------------------------------------------
+cnf(commutativity_of_add,axiom,
+ ( add(X,Y) = add(Y,X) )).
+
+cnf(commutativity_of_multiply,axiom,
+ ( multiply(X,Y) = multiply(Y,X) )).
+
+cnf(distributivity1,axiom,
+ ( add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)) )).
+
+cnf(distributivity2,axiom,
+ ( multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) )).
+
+cnf(additive_id1,axiom,
+ ( add(X,additive_identity) = X )).
+
+cnf(multiplicative_id1,axiom,
+ ( multiply(X,multiplicative_identity) = X )).
+
+cnf(additive_inverse1,axiom,
+ ( add(X,inverse(X)) = multiplicative_identity )).
+
+cnf(multiplicative_inverse1,axiom,
+ ( multiply(X,inverse(X)) = additive_identity )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000+0 : TPTP v5.5.0. Released v3.6.0.
+% Domain : Syntactic
+% Axioms : A simple include file for FOF
+% Version : Biased.
+% English :
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Syntax : Number of formulae : 3 ( 3 unit)
+% Number of atoms : 3 ( 0 equality)
+% Maximal formula depth : 1 ( 1 average)
+% Number of connectives : 0 ( 0 ~ ; 0 |; 0 &)
+% ( 0 <=>; 0 =>; 0 <=)
+% ( 0 <~>; 0 ~|; 0 ~&)
+% Number of predicates : 3 ( 3 propositional; 0-0 arity)
+% Number of functors : 0 ( 0 constant; --- arity)
+% Number of variables : 0 ( 0 singleton; 0 !; 0 ?)
+% Maximal term depth : 0 ( 0 average)
+% SPC :
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+fof(ia1,axiom,
+ ia1).
+
+fof(ia2,axiom,
+ ia2).
+
+fof(ia3,axiom,
+ ia3).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000-0 : TPTP v5.5.0. Released v3.6.0.
+% Domain : Syntactic
+% Axioms : A simple include file for CNF
+% Version : Biased.
+% English :
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 3 RR)
+% Number of atoms : 3 ( 0 equality)
+% Maximal clause size : 1 ( 1 average)
+% Number of predicates : 3 ( 3 propositional; 0-0 arity)
+% Number of functors : 0 ( 0 constant; --- arity)
+% Number of variables : 0 ( 0 singleton)
+% Maximal term depth : 0 ( 0 average)
+% SPC :
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+cnf(ia1,axiom,
+ ia1).
+
+cnf(ia2,axiom,
+ ia2).
+
+cnf(ia3,axiom,
+ ia3).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000_0 : TPTP v5.5.0. Released v5.0.0.
+% Domain : Syntactic
+% Axioms : A simple include file for TFF
+% Version : Biased.
+% English :
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Syntax : Number of formulae : 6 ( 6 unit; 3 type)
+% Number of atoms : 6 ( 0 equality)
+% Maximal formula depth : 2 ( 2 average)
+% Number of connectives : 0 ( 0 ~; 0 |; 0 &)
+% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
+% ( 0 ~|; 0 ~&)
+% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
+% Number of predicates : 4 ( 4 propositional; 0-0 arity)
+% Number of functors : 0 ( 0 constant; --- arity)
+% Number of variables : 0 ( 0 sgn; 0 !; 0 ?)
+% Maximal term depth : 0 ( 0 average)
+% SPC :
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Some axioms to include
+tff(ia1_type,type,(
+ ia1: $o )).
+
+tff(ia2_type,type,(
+ ia2: $o )).
+
+tff(ia3_type,type,(
+ ia3: $o )).
+
+tff(ia1,axiom,(
+ ia1 )).
+
+tff(ia2,axiom,(
+ ia2 )).
+
+tff(ia3,axiom,(
+ ia3 )).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : BOO003-4 : TPTP v5.5.0. Released v1.1.0.
+% Domain : Boolean Algebra
+% Problem : Multiplication is idempotent (X * X = X)
+% Version : [Ver94] (equality) axioms.
+% English :
+
+% Refs : [Ver94] Veroff (1994), Problem Set
+% Source : [Ver94]
+% Names : TA [Ver94]
+
+% Status : Unsatisfiable
+% Rating : 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v2.1.0, 0.13 v2.0.0
+% Syntax : Number of clauses : 9 ( 0 non-Horn; 9 unit; 1 RR)
+% Number of atoms : 9 ( 9 equality)
+% Maximal clause size : 1 ( 1 average)
+% Number of predicates : 1 ( 0 propositional; 2-2 arity)
+% Number of functors : 6 ( 3 constant; 0-2 arity)
+% Number of variables : 14 ( 0 singleton)
+% Maximal term depth : 3 ( 2 average)
+% SPC : CNF_UNS_RFO_PEQ_UEQ
+
+% Comments :
+%--------------------------------------------------------------------------
+%----Include boolean algebra axioms for equality formulation
+include('Axioms/BOO004-0.ax').
+%--------------------------------------------------------------------------
+cnf(prove_a_times_a_is_a,negated_conjecture,
+ ( multiply(a,a) != a )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : BOO027-1 : TPTP v5.5.0. Released v2.2.0.
+% Domain : Boolean Algebra
+% Problem : Independence of self-dual 2-basis.
+% Version : [MP96] (eqiality) axioms : Especial.
+% English : Show that half of the self-dual 2-basis in DUAL-BA-3 is not
+% a basis for Boolean Algebra.
+
+% Refs : [McC98] McCune (1998), Email to G. Sutcliffe
+% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq
+% Source : [McC98]
+% Names : DUAL-BA-4 [MP96]
+
+% Status : Satisfiable
+% Rating : 0.00 v5.5.0, 0.20 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.2.1
+% Syntax : Number of clauses : 6 ( 0 non-Horn; 6 unit; 1 RR)
+% Number of atoms : 6 ( 6 equality)
+% Maximal clause size : 1 ( 1 average)
+% Number of predicates : 1 ( 0 propositional; 2-2 arity)
+% Number of functors : 5 ( 2 constant; 0-2 arity)
+% Number of variables : 10 ( 0 singleton)
+% Maximal term depth : 5 ( 3 average)
+% SPC : CNF_SAT_RFO_PEQ_UEQ
+
+% Comments : There is a 2-element model.
+%--------------------------------------------------------------------------
+%----Two properties of Boolean algebra:
+cnf(multiply_add_property,axiom,
+ ( multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) )).
+
+cnf(additive_inverse,axiom,
+ ( add(X,inverse(X)) = one )).
+
+%----Pixley properties:
+cnf(pixley1,axiom,
+ ( add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y )).
+
+cnf(pixley2,axiom,
+ ( add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X )).
+
+cnf(pixley3,axiom,
+ ( add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X )).
+
+%----Denial of a property of Boolean Algebra:
+cnf(prove_idempotence,negated_conjecture,
+ ( add(a,a) != a )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : DAT001=1 : TPTP v5.5.0. Released v5.0.0.
+% Domain : Data Structures
+% Problem : Recursive list sort
+% Version : Especial.
+% English :
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Theorem
+% Rating : 0.12 v5.5.0, 0.25 v5.4.0, 0.38 v5.3.0, 0.29 v5.2.0, 0.20 v5.1.0, 0.25 v5.0.0
+% Syntax : Number of formulae : 8 ( 5 unit; 4 type)
+% Number of atoms : 13 ( 0 equality)
+% Maximal formula depth : 6 ( 3 average)
+% Number of connectives : 2 ( 0 ~; 0 |; 1 &)
+% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
+% ( 0 ~|; 0 ~&)
+% Number of type conns : 3 ( 2 >; 1 *; 0 +; 0 <<)
+% Number of predicates : 9 ( 7 propositional; 0-2 arity)
+% Number of functors : 7 ( 6 constant; 0-2 arity)
+% Number of variables : 4 ( 0 sgn; 4 !; 0 ?)
+% Maximal term depth : 6 ( 2 average)
+% Arithmetic symbols : 7 ( 2 pred; 0 func; 5 numbers)
+% SPC : TFF_THM_NEQ_ARI
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(list_type,type,(
+ list: $tType )).
+
+tff(nil_type,type,(
+ nil: list )).
+
+tff(mycons_type,type,(
+ mycons: ( $int * list ) > list )).
+
+tff(sorted_type,type,(
+ sorted: list > $o )).
+
+tff(empty_is_sorted,axiom,(
+ sorted(nil) )).
+
+tff(single_is_sorted,axiom,(
+ ! [X: $int] : sorted(mycons(X,nil)) )).
+
+tff(recursive_sort,axiom,(
+ ! [X: $int,Y: $int,R: list] :
+ ( ( $less(X,Y)
+ & sorted(mycons(Y,R)) )
+ => sorted(mycons(X,mycons(Y,R))) ) )).
+
+tff(check_list,conjecture,(
+ sorted(mycons(1,mycons(2,mycons(4,mycons(7,mycons(100,nil)))))) )).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : KRS018+1 : TPTP v5.5.0. Released v3.1.0.
+% Domain : Knowledge Representation (Semantic Web)
+% Problem : Nothing can be defined using OWL Lite restrictions
+% Version : Especial.
+% English :
+
+% Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe
+% : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW
+% Source : [Bec03]
+% Names : consistent_I5.2-Manifest001 [Bec03]
+
+% Status : Satisfiable
+% Rating : 0.00 v4.1.0, 0.25 v4.0.1, 0.00 v3.1.0
+% Syntax : Number of formulae : 4 ( 0 unit)
+% Number of atoms : 8 ( 0 equality)
+% Maximal formula depth : 5 ( 4 average)
+% Number of connectives : 7 ( 3 ~ ; 0 |; 1 &)
+% ( 1 <=>; 2 =>; 0 <=)
+% ( 0 <~>; 0 ~|; 0 ~&)
+% Number of predicates : 6 ( 0 propositional; 1-2 arity)
+% Number of functors : 0 ( 0 constant; --- arity)
+% Number of variables : 6 ( 0 singleton; 4 !; 2 ?)
+% Maximal term depth : 1 ( 1 average)
+% SPC : FOF_SAT_RFO_NEQ
+
+% Comments : Sean Bechhofer says there are some errors in the encoding of
+% datatypes, so this problem may not be perfect. At least it's
+% still representative of the type of reasoning required for OWL.
+%------------------------------------------------------------------------------
+%----Thing and Nothing
+fof(axiom_0,axiom,
+ ( ! [X] :
+ ( cowlThing(X)
+ & ~ cowlNothing(X) ) )).
+
+%----String and Integer disjoint
+fof(axiom_1,axiom,
+ ( ! [X] :
+ ( xsd_string(X)
+ <=> ~ xsd_integer(X) ) )).
+
+%----Super cNothing
+fof(axiom_2,axiom,
+ ( ! [X] :
+ ( cNothing(X)
+ => ~ ( ? [Y] : rp(X,Y) ) ) )).
+
+%----Super cNothing
+fof(axiom_3,axiom,
+ ( ! [X] :
+ ( cNothing(X)
+ => ? [Y0] : rp(X,Y0) ) )).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : KRS063+1 : TPTP v5.5.0. Released v3.1.0.
+% Domain : Knowledge Representation (Semantic Web)
+% Problem : An example combining owl:oneOf and owl:inverseOf
+% Version : Especial.
+% English :
+
+% Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe
+% : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW
+% Source : [Bec03]
+% Names : inconsistent_I4.5-Manifest002 [Bec03]
+
+% Status : Unsatisfiable
+% Rating : 0.00 v3.1.0
+% Syntax : Number of formulae : 27 ( 9 unit)
+% Number of atoms : 63 ( 18 equality)
+% Maximal formula depth : 8 ( 4 average)
+% Number of connectives : 39 ( 3 ~ ; 5 |; 14 &)
+% ( 4 <=>; 13 =>; 0 <=)
+% ( 0 <~>; 0 ~|; 0 ~&)
+% Number of predicates : 11 ( 0 propositional; 1-2 arity)
+% Number of functors : 7 ( 7 constant; 0-0 arity)
+% Number of variables : 37 ( 0 singleton; 36 !; 1 ?)
+% Maximal term depth : 1 ( 1 average)
+% SPC : FOF_UNS_RFO_SEQ
+
+% Comments : Sean Bechhofer says there are some errors in the encoding of
+% datatypes, so this problem may not be perfect. At least it's
+% still representative of the type of reasoning required for OWL.
+%------------------------------------------------------------------------------
+fof(cEUCountry_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & cEUCountry(A) )
+ => cEUCountry(B) ) )).
+
+fof(cEuroMP_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & cEuroMP(A) )
+ => cEuroMP(B) ) )).
+
+fof(cEuropeanCountry_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & cEuropeanCountry(A) )
+ => cEuropeanCountry(B) ) )).
+
+fof(cPerson_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & cPerson(A) )
+ => cPerson(B) ) )).
+
+fof(cowlNothing_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & cowlNothing(A) )
+ => cowlNothing(B) ) )).
+
+fof(cowlThing_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & cowlThing(A) )
+ => cowlThing(B) ) )).
+
+fof(rhasEuroMP_substitution_1,axiom,
+ ( ! [A,B,C] :
+ ( ( A = B
+ & rhasEuroMP(A,C) )
+ => rhasEuroMP(B,C) ) )).
+
+fof(rhasEuroMP_substitution_2,axiom,
+ ( ! [A,B,C] :
+ ( ( A = B
+ & rhasEuroMP(C,A) )
+ => rhasEuroMP(C,B) ) )).
+
+fof(risEuroMPFrom_substitution_1,axiom,
+ ( ! [A,B,C] :
+ ( ( A = B
+ & risEuroMPFrom(A,C) )
+ => risEuroMPFrom(B,C) ) )).
+
+fof(risEuroMPFrom_substitution_2,axiom,
+ ( ! [A,B,C] :
+ ( ( A = B
+ & risEuroMPFrom(C,A) )
+ => risEuroMPFrom(C,B) ) )).
+
+fof(xsd_integer_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & xsd_integer(A) )
+ => xsd_integer(B) ) )).
+
+fof(xsd_string_substitution_1,axiom,
+ ( ! [A,B] :
+ ( ( A = B
+ & xsd_string(A) )
+ => xsd_string(B) ) )).
+
+%----Thing and Nothing
+fof(axiom_0,axiom,
+ ( ! [X] :
+ ( cowlThing(X)
+ & ~ cowlNothing(X) ) )).
+
+%----String and Integer disjoint
+fof(axiom_1,axiom,
+ ( ! [X] :
+ ( xsd_string(X)
+ <=> ~ xsd_integer(X) ) )).
+
+%----Enumeration cEUCountry
+fof(axiom_2,axiom,
+ ( ! [X] :
+ ( cEUCountry(X)
+ <=> ( X = iPT
+ | X = iBE
+ | X = iNL
+ | X = iES
+ | X = iFR
+ | X = iUK ) ) )).
+
+%----Equality cEuroMP
+fof(axiom_3,axiom,
+ ( ! [X] :
+ ( cEuroMP(X)
+ <=> ? [Y] :
+ ( risEuroMPFrom(X,Y)
+ & cowlThing(Y) ) ) )).
+
+%----Domain: rhasEuroMP
+fof(axiom_4,axiom,
+ ( ! [X,Y] :
+ ( rhasEuroMP(X,Y)
+ => cEUCountry(X) ) )).
+
+%----Inverse: risEuroMPFrom
+fof(axiom_5,axiom,
+ ( ! [X,Y] :
+ ( risEuroMPFrom(X,Y)
+ <=> rhasEuroMP(Y,X) ) )).
+
+%----iBE
+fof(axiom_6,axiom,
+ ( cEuropeanCountry(iBE) )).
+
+%----iES
+fof(axiom_7,axiom,
+ ( cEuropeanCountry(iES) )).
+
+%----iFR
+fof(axiom_8,axiom,
+ ( cEuropeanCountry(iFR) )).
+
+%----iKinnock
+fof(axiom_9,axiom,
+ ( cPerson(iKinnock) )).
+
+%----iKinnock
+fof(axiom_10,axiom,
+ ( ~ cEuroMP(iKinnock) )).
+
+%----iNL
+fof(axiom_11,axiom,
+ ( cEuropeanCountry(iNL) )).
+
+%----iPT
+fof(axiom_12,axiom,
+ ( cEuropeanCountry(iPT) )).
+
+%----iUK
+fof(axiom_13,axiom,
+ ( cEuropeanCountry(iUK) )).
+
+fof(axiom_14,axiom,
+ ( rhasEuroMP(iUK,iKinnock) )).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : MGT019+2 : TPTP v5.5.0. Released v2.0.0.
+% Domain : Management (Organisation Theory)
+% Problem : Growth rate of EPs exceeds that of FMs in stable environments
+% Version : [PM93] axioms.
+% English : The growth rate of efficent producers exceeds the growth rate
+% of first movers past a certain time in stable environments.
+
+% Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg
+% : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg
+% : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing
+% Source : [PM93]
+% Names : LEMMA 1 [PM93]
+% : L1 [PB+94]
+
+% Status : CounterSatisfiable
+% Rating : 0.00 v4.1.0, 0.20 v4.0.1, 0.00 v3.5.0, 0.33 v3.4.0, 0.00 v2.1.0
+% Syntax : Number of formulae : 5 ( 0 unit)
+% Number of atoms : 21 ( 1 equality)
+% Maximal formula depth : 8 ( 6 average)
+% Number of connectives : 17 ( 1 ~ ; 1 |; 8 &)
+% ( 0 <=>; 7 =>; 0 <=)
+% ( 0 <~>; 0 ~|; 0 ~&)
+% Number of predicates : 7 ( 0 propositional; 1-4 arity)
+% Number of functors : 5 ( 2 constant; 0-2 arity)
+% Number of variables : 11 ( 0 singleton; 9 !; 2 ?)
+% Maximal term depth : 2 ( 1 average)
+% SPC : FOF_CSA_RFO_SEQ
+
+% Comments : There is no MGT019+1 as Kamps did not send it to me.
+%--------------------------------------------------------------------------
+%----Subsitution axioms
+%----Problem axioms
+%----L2. The disbanding rate of first movers exceeds the disbanding
+%----rate of efficient producers.
+fof(l2,axiom,
+ ( ~ ( ! [E,T] :
+ ( ( environment(E)
+ & subpopulations(first_movers,efficient_producers,E,T) )
+ => greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)) ) ) )).
+
+%----If EP have lower disbanding rate and not lower founding rate than
+%----FM, then EP have higher growth rate.
+fof(mp_EP_lower_disbanding_rate,axiom,
+ ( ! [T] :
+ ( ( greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T))
+ & greater_or_equal(founding_rate(efficient_producers,T),founding_rate(first_movers,T)) )
+ => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) )).
+
+%----MP. on "greater or equal to"
+fof(mp_greater_or_equal,axiom,
+ ( ! [X,Y] :
+ ( greater_or_equal(X,Y)
+ => ( greater(X,Y)
+ | X = Y ) ) )).
+
+%----A8. The founding rate of first movers does not exceed the founding
+%----rate of efficient producers past a certain point in a stable
+%----environment.
+fof(a8,hypothesis,
+ ( ! [E] :
+ ( ( environment(E)
+ & stable(E) )
+ => ? [To] :
+ ( in_environment(E,To)
+ & ! [T] :
+ ( ( subpopulations(first_movers,efficient_producers,E,T)
+ & greater_or_equal(T,To) )
+ => greater_or_equal(founding_rate(efficient_producers,T),founding_rate(first_movers,T)) ) ) ) )).
+
+%----GOAL: L1. The growth rate of efficient producers exceeds the growth
+%----rate of first movers past a certain time in stable environments.
+fof(prove_l1,conjecture,
+ ( ! [E] :
+ ( ( environment(E)
+ & stable(E) )
+ => ? [To] :
+ ( in_environment(E,To)
+ & ! [T] :
+ ( ( subpopulations(first_movers,efficient_producers,E,T)
+ & greater_or_equal(T,To) )
+ => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : MGT031-1 : TPTP v5.5.0. Released v2.4.0.
+% Domain : Management (Organisation Theory)
+% Problem : First movers appear first in an environment
+% Version : [PB+94] axioms : Reduced & Augmented > Complete.
+% English :
+
+% Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg
+% : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg
+% : [Kam95] Kamps (1995), Email to G. Sutcliffe
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Rating : 0.00 v2.5.0, 0.17 v2.4.0
+% Syntax : Number of clauses : 15 ( 2 non-Horn; 3 unit; 15 RR)
+% Number of atoms : 38 ( 5 equality)
+% Maximal clause size : 5 ( 3 average)
+% Number of predicates : 6 ( 0 propositional; 1-3 arity)
+% Number of functors : 10 ( 6 constant; 0-2 arity)
+% Number of variables : 23 ( 0 singleton)
+% Maximal term depth : 3 ( 1 average)
+% SPC : CNF_SAT_RFO_EQU_NUE
+
+% Comments : Created with tptp2X -f tptp -t clausify:otter MGT031+1.p
+%--------------------------------------------------------------------------
+cnf(mp_positive_number_when_appear_20,axiom,
+ ( ~ environment(A)
+ | greater(number_of_organizations(e,appear(an_organisation,A)),zero) )).
+
+cnf(mp_number_mean_non_empty_21,axiom,
+ ( ~ environment(A)
+ | ~ greater(number_of_organizations(A,B),zero)
+ | subpopulation(sk1(B,A),A,B) )).
+
+cnf(mp_number_mean_non_empty_22,axiom,
+ ( ~ environment(A)
+ | ~ greater(number_of_organizations(A,B),zero)
+ | greater(cardinality_at_time(sk1(B,A),B),zero) )).
+
+cnf(mp_no_EP_before_appearance_23,axiom,
+ ( ~ environment(A)
+ | ~ in_environment(A,B)
+ | ~ greater(appear(efficient_producers,A),B)
+ | ~ greater(cardinality_at_time(efficient_producers,B),zero) )).
+
+cnf(mp_no_FM_before_appearance_24,axiom,
+ ( ~ environment(A)
+ | ~ in_environment(A,B)
+ | ~ greater(appear(first_movers,A),B)
+ | ~ greater(cardinality_at_time(first_movers,B),zero) )).
+
+cnf(mp_FM_not_precede_first_25,axiom,
+ ( ~ environment(A)
+ | greater_or_equal(appear(first_movers,A),appear(an_organisation,A)) )).
+
+cnf(mp_greater_transitivity_26,axiom,
+ ( ~ greater(A,B)
+ | ~ greater(B,C)
+ | greater(A,C) )).
+
+cnf(mp_greater_or_equal_27,axiom,
+ ( ~ greater_or_equal(A,B)
+ | greater(A,B)
+ | A = B )).
+
+cnf(mp_greater_or_equal_28,axiom,
+ ( ~ greater(A,B)
+ | greater_or_equal(A,B) )).
+
+cnf(mp_greater_or_equal_29,axiom,
+ ( A != B
+ | greater_or_equal(A,B) )).
+
+cnf(a9_30,hypothesis,
+ ( ~ environment(A)
+ | ~ subpopulation(B,A,C)
+ | ~ greater(cardinality_at_time(B,C),zero)
+ | B = efficient_producers
+ | B = first_movers )).
+
+cnf(a13_31,hypothesis,
+ ( ~ environment(A)
+ | greater(appear(efficient_producers,e),appear(first_movers,A)) )).
+
+cnf(prove_l13_32,negated_conjecture,
+ ( environment(sk2) )).
+
+cnf(prove_l13_33,negated_conjecture,
+ ( in_environment(sk2,appear(an_organisation,sk2)) )).
+
+cnf(prove_l13_34,negated_conjecture,
+ ( appear(an_organisation,sk2) != appear(first_movers,sk2) )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : MGT041-2 : TPTP v5.5.0. Released v2.4.0.
+% Domain : Management (Organisation Theory)
+% Problem : There are non-FM and non-EP organisations
+% Version : [PM93] axioms.
+% English : There are non-first mover and non-efficient producers
+% organisations.
+
+% Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg
+% : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg
+% : [Kam95] Kamps (1995), Email to G. Sutcliffe
+% Source : [TPTP]
+% Names :
+
+% Status : Unsatisfiable
+% Rating : 0.00 v2.4.0
+% Syntax : Number of clauses : 8 ( 1 non-Horn; 4 unit; 8 RR)
+% Number of atoms : 17 ( 0 equality)
+% Maximal clause size : 4 ( 2 average)
+% Number of predicates : 6 ( 0 propositional; 1-3 arity)
+% Number of functors : 4 ( 4 constant; 0-0 arity)
+% Number of variables : 8 ( 1 singleton)
+% Maximal term depth : 1 ( 1 average)
+% SPC : CNF_UNS_EPR
+
+% Comments : Created with tptp2X -f tptp -t clausify:otter MGT041+2.p
+%--------------------------------------------------------------------------
+cnf(mp_not_high_and_low_1,axiom,
+ ( ~ number_of_routines(A,B,low)
+ | ~ number_of_routines(A,B,high) )).
+
+cnf(a14_2,hypothesis,
+ ( ~ organisation_at_time(A,B)
+ | ~ efficient_producer(A)
+ | ~ founding_time(A,B)
+ | has_elaborated_routines(A,B) )).
+
+cnf(a15_3,hypothesis,
+ ( ~ organisation_at_time(A,B)
+ | ~ first_mover(A)
+ | ~ founding_time(A,B)
+ | number_of_routines(A,B,low) )).
+
+cnf(a16_4,hypothesis,
+ ( organisation_at_time(sk1,sk2) )).
+
+cnf(a16_5,hypothesis,
+ ( founding_time(sk1,sk2) )).
+
+cnf(a16_6,hypothesis,
+ ( number_of_routines(sk1,sk2,high) )).
+
+cnf(a16_7,hypothesis,
+ ( ~ has_elaborated_routines(sk1,sk2) )).
+
+cnf(prove_t10_8,negated_conjecture,
+ ( ~ organisation_at_time(A,B)
+ | first_mover(A)
+ | efficient_producer(A) )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+topdir = ../../../..
+srcdir = test/regress/regress0/tptp
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
--- /dev/null
+BINARY = cvc4
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+ $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \
+ $(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+# escape the `=' in file names
+equals = =
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS = \
+ tptp_parser.p \
+ tptp_parser2.p \
+ tptp_parser3.p \
+ tptp_parser4.p \
+ tptp_parser5.p \
+ tptp_parser6.p \
+ tptp_parser7.p \
+ tptp_parser8.p \
+ tptp_parser9.p \
+ tptp_parser10.p \
+ tff0.p \
+ tff0-arith.p \
+ ARI086$(equals)1.p \
+ BOO003-4.p \
+ DAT001$(equals)1.p \
+ KRS018+1.p \
+ KRS063+1.p \
+ MGT019+2.p \
+ MGT041-2.p \
+ PUZ131_1.p \
+ SYN000+1.p \
+ SYN000+2.p \
+ SYN000-1.p \
+ SYN000-2.p \
+ SYN000$(equals)2.p \
+ SYN000_1.p \
+ SYN000_2.p \
+ SYN075-1.p
+
+# axiom files required for the above tests
+TEST_DEPS_DIST = \
+ Axioms/BOO004-0.ax \
+ Axioms/SYN000_0.ax \
+ Axioms/SYN000-0.ax \
+ Axioms/SYN000+0.ax
+
+# these take too long at present
+EXTRA_DIST = $(TESTS) \
+ $(TEST_DEPS_DIST) \
+ BOO027-1.p \
+ MGT031-1.p \
+ NLP114-1.p \
+ SYN075+1.p
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+# error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+# error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
--- /dev/null
+%--------------------------------------------------------------------------
+% File : NLP114-1 : TPTP v5.5.0. Released v2.4.0.
+% Domain : Natural Language Processing
+% Problem : An old dirty white Chevy, problem 1
+% Version : [Bos00b] axioms.
+% English : Eliminating logically equivalent interpretations in the statement
+% "An old dirty white chevy barrels down a lonely street in
+% hollywood."
+
+% Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a
+% [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Rating : 0.00 v2.4.0
+% Syntax : Number of clauses : 36 ( 16 non-Horn; 2 unit; 36 RR)
+% Number of atoms : 102 ( 0 equality)
+% Maximal clause size : 18 ( 3 average)
+% Number of predicates : 18 ( 1 propositional; 0-3 arity)
+% Number of functors : 11 ( 11 constant; 0-0 arity)
+% Number of variables : 11 ( 0 singleton)
+% Maximal term depth : 1 ( 1 average)
+% SPC : CNF_SAT_EPR
+
+% Comments : Created from NLP114+1.p using FLOTTER
+%--------------------------------------------------------------------------
+cnf(clause1,negated_conjecture,
+ ( actual_world(skc17) )).
+
+cnf(clause2,negated_conjecture,
+ ( actual_world(skc11) )).
+
+cnf(clause3,negated_conjecture,
+ ( ssSkC0
+ | city(skc17,skc20) )).
+
+cnf(clause4,negated_conjecture,
+ ( ssSkC0
+ | street(skc17,skc20) )).
+
+cnf(clause5,negated_conjecture,
+ ( ssSkC0
+ | lonely(skc17,skc20) )).
+
+cnf(clause6,negated_conjecture,
+ ( ssSkC0
+ | placename(skc17,skc21) )).
+
+cnf(clause7,negated_conjecture,
+ ( ssSkC0
+ | hollywood_placename(skc17,skc21) )).
+
+cnf(clause8,negated_conjecture,
+ ( ssSkC0
+ | event(skc17,skc18) )).
+
+cnf(clause9,negated_conjecture,
+ ( ssSkC0
+ | present(skc17,skc18) )).
+
+cnf(clause10,negated_conjecture,
+ ( ssSkC0
+ | barrel(skc17,skc18) )).
+
+cnf(clause11,negated_conjecture,
+ ( ssSkC0
+ | old(skc17,skc19) )).
+
+cnf(clause12,negated_conjecture,
+ ( ssSkC0
+ | dirty(skc17,skc19) )).
+
+cnf(clause13,negated_conjecture,
+ ( ssSkC0
+ | white(skc17,skc19) )).
+
+cnf(clause14,negated_conjecture,
+ ( ssSkC0
+ | chevy(skc17,skc19) )).
+
+cnf(clause15,negated_conjecture,
+ ( ~ ssSkC0
+ | lonely(skc11,skc16) )).
+
+cnf(clause16,negated_conjecture,
+ ( ~ ssSkC0
+ | street(skc11,skc16) )).
+
+cnf(clause17,negated_conjecture,
+ ( ~ ssSkC0
+ | barrel(skc11,skc12) )).
+
+cnf(clause18,negated_conjecture,
+ ( ~ ssSkC0
+ | present(skc11,skc12) )).
+
+cnf(clause19,negated_conjecture,
+ ( ~ ssSkC0
+ | event(skc11,skc12) )).
+
+cnf(clause20,negated_conjecture,
+ ( ~ ssSkC0
+ | hollywood_placename(skc11,skc14) )).
+
+cnf(clause21,negated_conjecture,
+ ( ~ ssSkC0
+ | placename(skc11,skc14) )).
+
+cnf(clause22,negated_conjecture,
+ ( ~ ssSkC0
+ | city(skc11,skc15) )).
+
+cnf(clause23,negated_conjecture,
+ ( ~ ssSkC0
+ | chevy(skc11,skc13) )).
+
+cnf(clause24,negated_conjecture,
+ ( ~ ssSkC0
+ | white(skc11,skc13) )).
+
+cnf(clause25,negated_conjecture,
+ ( ~ ssSkC0
+ | dirty(skc11,skc13) )).
+
+cnf(clause26,negated_conjecture,
+ ( ~ ssSkC0
+ | old(skc11,skc13) )).
+
+cnf(clause27,negated_conjecture,
+ ( ssSkC0
+ | down(skc17,skc18,skc20) )).
+
+cnf(clause28,negated_conjecture,
+ ( ssSkC0
+ | in(skc17,skc18,skc20) )).
+
+cnf(clause29,negated_conjecture,
+ ( ssSkC0
+ | of(skc17,skc21,skc20) )).
+
+cnf(clause30,negated_conjecture,
+ ( ssSkC0
+ | agent(skc17,skc18,skc19) )).
+
+cnf(clause31,negated_conjecture,
+ ( ~ ssSkC0
+ | down(skc11,skc12,skc16) )).
+
+cnf(clause32,negated_conjecture,
+ ( ~ ssSkC0
+ | in(skc11,skc12,skc15) )).
+
+cnf(clause33,negated_conjecture,
+ ( ~ ssSkC0
+ | of(skc11,skc14,skc15) )).
+
+cnf(clause34,negated_conjecture,
+ ( ~ ssSkC0
+ | agent(skc11,skc12,skc13) )).
+
+cnf(clause35,negated_conjecture,
+ ( ~ down(U,V,W)
+ | ~ lonely(U,W)
+ | ~ street(U,W)
+ | ~ barrel(U,V)
+ | ~ present(U,V)
+ | ~ event(U,V)
+ | ~ hollywood_placename(U,X)
+ | ~ placename(U,X)
+ | ~ in(U,V,Y)
+ | ~ city(U,Y)
+ | ~ of(U,X,Y)
+ | ~ chevy(U,Z)
+ | ~ white(U,Z)
+ | ~ dirty(U,Z)
+ | ~ old(U,Z)
+ | ~ agent(U,V,Z)
+ | ~ actual_world(U)
+ | ssSkC0 )).
+
+cnf(clause36,negated_conjecture,
+ ( ~ city(U,V)
+ | ~ street(U,V)
+ | ~ lonely(U,V)
+ | ~ down(U,W,V)
+ | ~ in(U,W,V)
+ | ~ placename(U,X)
+ | ~ hollywood_placename(U,X)
+ | ~ of(U,X,V)
+ | ~ event(U,W)
+ | ~ present(U,W)
+ | ~ barrel(U,W)
+ | ~ agent(U,W,Y)
+ | ~ old(U,Y)
+ | ~ dirty(U,Y)
+ | ~ white(U,Y)
+ | ~ chevy(U,Y)
+ | ~ actual_world(U)
+ | ~ ssSkC0 )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : PUZ131_1 : TPTP v5.5.0. Released v5.0.0.
+% Domain : Puzzles
+% Problem : Victor teaches Michael
+% Version : Especial.
+% English : Every student is enrolled in at least one course. Every professor
+% teaches at least one course. Every course has at least one student
+% enrolled. Every course has at least one professor teaching. The
+% coordinator of a course teaches the course. If a student is
+% enroled in a course then the student is taught by every professor
+% who teaches the course. Michael is enrolled in CSC410. Victor is
+% the coordinator of CSC410. Therefore, Michael is taught by Victor.
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Theorem
+% Rating : 0.00 v5.0.0
+% Syntax : Number of formulae : 19 ( 14 unit; 10 type)
+% Number of atoms : 28 ( 1 equality)
+% Maximal formula depth : 6 ( 3 average)
+% Number of connectives : 2 ( 0 ~; 0 |; 0 &)
+% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
+% ( 0 ~|; 0 ~&)
+% Number of type conns : 7 ( 4 >; 3 *; 0 +; 0 <<)
+% Number of predicates : 16 ( 12 propositional; 0-2 arity)
+% Number of functors : 4 ( 3 constant; 0-1 arity)
+% Number of variables : 12 ( 0 sgn; 8 !; 4 ?)
+% Maximal term depth : 2 ( 1 average)
+% SPC : TFF_THM_EQU_NAR
+
+% Comments :
+%------------------------------------------------------------------------------
+tff(student_type,type,(
+ student: $tType )).
+
+tff(professor_type,type,(
+ professor: $tType )).
+
+tff(course_type,type,(
+ course: $tType )).
+
+tff(michael_type,type,(
+ michael: student )).
+
+tff(victor_type,type,(
+ victor: professor )).
+
+tff(csc410_type,type,(
+ csc410: course )).
+
+tff(enrolled_type,type,(
+ enrolled: ( student * course ) > $o )).
+
+tff(teaches_type,type,(
+ teaches: ( professor * course ) > $o )).
+
+tff(taught_by_type,type,(
+ taughtby: ( student * professor ) > $o )).
+
+tff(coordinator_of_type,type,(
+ coordinatorof: course > professor )).
+
+tff(student_enrolled_axiom,axiom,(
+ ! [X: student] :
+ ? [Y: course] : enrolled(X,Y) )).
+
+tff(professor_teaches,axiom,(
+ ! [X: professor] :
+ ? [Y: course] : teaches(X,Y) )).
+
+tff(course_enrolled,axiom,(
+ ! [X: course] :
+ ? [Y: student] : enrolled(Y,X) )).
+
+tff(course_teaches,axiom,(
+ ! [X: course] :
+ ? [Y: professor] : teaches(Y,X) )).
+
+tff(coordinator_teaches,axiom,(
+ ! [X: course] : teaches(coordinatorof(X),X) )).
+
+tff(student_enrolled_taught,axiom,(
+ ! [X: student,Y: course] :
+ ( enrolled(X,Y)
+ => ! [Z: professor] :
+ ( teaches(Z,Y)
+ => taughtby(X,Z) ) ) )).
+
+tff(michael_enrolled_csc410_axiom,axiom,(
+ enrolled(michael,csc410) )).
+
+tff(victor_coordinator_csc410_axiom,axiom,(
+ coordinatorof(csc410) = victor )).
+
+tff(teaching_conjecture,conjecture,(
+ taughtby(michael,victor) )).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000+1 : TPTP v5.5.0. Released v4.0.0.
+% Domain : Syntactic
+% Problem : Basic TPTP FOF syntax
+% Version : Biased.
+% English : Basic TPTP FOF syntax that you can't survive without parsing.
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Theorem
+% Rating : 0.43 v5.5.0, 0.48 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0
+% Syntax : Number of formulae : 12 ( 5 unit)
+% Number of atoms : 31 ( 3 equality)
+% Maximal formula depth : 7 ( 4 average)
+% Number of connectives : 28 ( 9 ~; 10 |; 3 &)
+% ( 1 <=>; 3 =>; 1 <=)
+% ( 1 <~>; 0 ~|; 0 ~&)
+% Number of predicates : 16 ( 10 propositional; 0-3 arity)
+% Number of functors : 8 ( 5 constant; 0-3 arity)
+% Number of variables : 13 ( 0 sgn; 5 !; 8 ?)
+% Maximal term depth : 4 ( 2 average)
+% SPC : FOF_THM_RFO_SEQ
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Propositional
+fof(propositional,axiom,
+ ( ( p0
+ & ~ q0 )
+ => ( r0
+ | ~ s0 ) )).
+
+%----First-order
+fof(first_order,axiom,(
+ ! [X] :
+ ( ( p(X)
+ | ~ q(X,a) )
+ => ? [Y,Z] :
+ ( r(X,f(Y),g(X,f(Y),Z))
+ & ~ s(f(f(f(b)))) ) ) )).
+
+%----Equality
+fof(equality,axiom,(
+ ? [Y] :
+ ! [X,Z] :
+ ( f(Y) = g(X,f(Y),Z)
+ | f(f(f(b))) != a
+ | X = f(Y) ) )).
+
+%----True and false
+fof(true_false,axiom,
+ ( $true
+ | $false )).
+
+%----Quoted symbols
+fof(single_quoted,axiom,
+ ( 'A proposition'
+ | 'A predicate'(a)
+ | p('A constant')
+ | p('A function'(a))
+ | p('A \'quoted \\ escape\'') )).
+
+%----Connectives - seen |, &, =>, ~ already
+fof(useful_connectives,axiom,(
+ ! [X] :
+ ( ( p(X)
+ <= ~ q(X,a) )
+ <=> ? [Y,Z] :
+ ( r(X,f(Y),g(X,f(Y),Z))
+ <~> ~ s(f(f(f(b)))) ) ) )).
+
+%----Annotated formula names
+fof(123,axiom,(
+ ! [X] :
+ ( ( p(X)
+ | ~ q(X,a) )
+ => ? [Y,Z] :
+ ( r(X,f(Y),g(X,f(Y),Z))
+ & ~ s(f(f(f(b)))) ) ) )).
+
+%----Roles
+fof(role_hypothesis,hypothesis,(
+ p(h) )).
+
+fof(role_conjecture,conjecture,(
+ ? [X] : p(X) )).
+
+%----Include directive
+include('Axioms/SYN000+0.ax').
+
+%----Comments
+/* This
+ is a block
+ comment.
+*/
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000+2 : TPTP v5.5.0. Bugfixed v4.1.1.
+% Domain : Syntactic
+% Problem : Advanced TPTP FOF syntax
+% Version : Biased.
+% English : Advanced TPTP FOF syntax that you will encounter some time.
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Rating : 0.50 v5.5.0, 0.67 v5.2.0, 1.00 v5.0.0
+% Syntax : Number of formulae : 20 ( 16 unit)
+% Number of atoms : 31 ( 2 equality)
+% Maximal formula depth : 7 ( 2 average)
+% Number of connectives : 13 ( 2 ~; 9 |; 0 &)
+% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
+% ( 1 ~|; 1 ~&)
+% Number of predicates : 8 ( 3 propositional; 0-3 arity)
+% Number of functors : 22 ( 20 constant; 0-3 arity)
+% Number of variables : 8 ( 0 sgn; 8 !; 0 ?)
+% Maximal term depth : 2 ( 1 average)
+% Arithmetic symbols : 12 ( 0 pred; 0 func; 12 numbers)
+% SPC : FOF_SAT_RFO_SEQ
+
+% Comments :
+% Bugfixes : v4.0.1 - Added more numbers, particularly rationals.
+% : v4.1.1 - Removed rationals with negative denominators.
+%------------------------------------------------------------------------------
+%----Quoted symbols
+fof(distinct_object,axiom,(
+ "An Apple" != "A \"Microsoft \\ escape\"" )).
+
+%----Numbers
+fof(integers,axiom,
+ ( p(12)
+ | p(-12) )).
+
+fof(rationals,axiom,
+ ( p(123/456)
+ | p(-123/456)
+ | p(+123/456) )).
+
+fof(reals,axiom,
+ ( p(123.456 )
+ | p(-123.456 )
+ | p(123.456E789 )
+ | p(123.456e789 )
+ | p(-123.456E789 )
+ | p(123.456E-789 )
+ | p(-123.456E-789 ) )).
+
+%----Connectives - seen |, &, =>, ~ already
+fof(never_used_connectives,axiom,(
+ ! [X] :
+ ( ( p(X)
+ ~| ~ q(X,a) )
+ ~& p(X) ) )).
+
+%----Roles
+fof(role_definition,definition,(
+ ! [X] : f(d) = f(X) )).
+
+fof(role_assumption,assumption,(
+ p(a) )).
+
+fof(role_lemma,lemma,(
+ p(l) )).
+
+fof(role_theorem,theorem,(
+ p(t) )).
+
+fof(role_unknown,unknown,(
+ p(u) )).
+
+%----Selective include directive
+include('Axioms/SYN000+0.ax',[ia1,ia3]).
+
+%----Source
+fof(source_unknown,axiom,(
+ ! [X] : p(X) ),
+ unknown).
+
+fof(source,axiom,(
+ ! [X] : p(X) ),
+ file('SYN000-1.p')).
+
+fof(source_name,axiom,(
+ ! [X] : p(X) ),
+ file('SYN000-1.p',source_unknown)).
+
+fof(source_copy,axiom,(
+ ! [X] : p(X) ),
+ source_unknown).
+
+fof(source_introduced_assumption,axiom,(
+ ! [X] : p(X) ),
+ introduced(assumption,[from,the,world])).
+
+fof(source_inference,plain,(
+ p(a) ),
+ inference(magic,
+ [status(thm),assumptions([source_introduced_assumption])],
+ [theory(equality),source_unknown])).
+
+fof(source_inference_with_bind,plain,(
+ p(a) ),
+ inference(magic,
+ [status(thm)],
+ [theory(equality),source_unknown:[bind(X,$fot(a))]])).
+
+%----Useful info
+fof(useful_info,axiom,(
+ ! [X] : p(X) ),
+ unknown,
+ [simple,
+ prolog(like,Data,[nested,12.2]),
+ AVariable,
+ 12.2,
+ "A distinct object",
+ $fof(p(X) | ~ q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b))))),
+ data(name):[colon,list,2],
+ [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]
+ ]).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000-1 : TPTP v5.5.0. Released v4.0.0.
+% Domain : Syntactic
+% Problem : Basic TPTP CNF syntax
+% Version : Biased.
+% English : Basic TPTP CNF syntax that you can't survive without parsing.
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Unsatisfiable
+% Rating : 0.50 v5.4.0, 0.55 v5.3.0, 0.56 v5.2.0, 0.62 v5.1.0, 0.65 v5.0.0, 0.64 v4.1.0, 0.62 v4.0.1, 0.64 v4.0.0
+% Syntax : Number of clauses : 11 ( 6 non-Horn; 5 unit; 7 RR)
+% Number of atoms : 27 ( 3 equality)
+% Maximal clause size : 5 ( 2 average)
+% Number of predicates : 16 ( 10 propositional; 0-3 arity)
+% Number of functors : 8 ( 5 constant; 0-3 arity)
+% Number of variables : 11 ( 5 singleton)
+% Maximal term depth : 4 ( 2 average)
+% SPC : CNF_UNS_RFO_SEQ_NHN
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Propositional
+cnf(propositional,axiom,
+ ( p0
+ | ~ q0
+ | r0
+ | ~ s0 )).
+
+%----First-order
+cnf(first_order,axiom,
+ ( p(X)
+ | ~ q(X,a)
+ | r(X,f(Y),g(X,f(Y),Z))
+ | ~ s(f(f(f(b)))) )).
+
+%----Equality
+cnf(equality,axiom,
+ ( f(Y) = g(X,f(Y),Z)
+ | f(f(f(b))) != a
+ | X = f(Y) )).
+
+%----True and false
+cnf(true_false,axiom,
+ ( $true
+ | $false )).
+
+%----Quoted symbols
+cnf(single_quoted,axiom,
+ ( 'A proposition'
+ | 'A predicate'(Y)
+ | p('A constant')
+ | p('A function'(a))
+ | p('A \'quoted \\ escape\'') )).
+
+%----Connectives - seen them all already
+
+%----Annotated formula names
+cnf(123,axiom,
+ ( p(X)
+ | ~ q(X,a)
+ | r(X,f(Y),g(X,f(Y),Z))
+ | ~ s(f(f(f(b)))) )).
+
+%----Roles - seen axiom already
+cnf(role_hypothesis,hypothesis,
+ p(h)).
+
+cnf(role_negated_conjecture,negated_conjecture,
+ ~ p(X)).
+
+%----Include directive
+include('Axioms/SYN000-0.ax').
+
+%----Comments
+/* This
+ is a block
+ comment.
+*/
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000-2 : TPTP v5.5.0. Bugfixed v4.1.1.
+% Domain : Syntactic
+% Problem : Advanced TPTP CNF syntax
+% Version : Biased.
+% English : Advanced TPTP CNF syntax that you will encounter some time.
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Rating : 1.00 v5.4.0, 0.90 v5.3.0, 0.89 v5.2.0, 0.90 v5.0.0
+% Syntax : Number of clauses : 19 ( 3 non-Horn; 16 unit; 12 RR)
+% Number of atoms : 28 ( 2 equality)
+% Maximal clause size : 7 ( 1 average)
+% Number of predicates : 8 ( 3 propositional; 0-3 arity)
+% Number of functors : 22 ( 20 constant; 0-3 arity)
+% Number of variables : 7 ( 7 singleton)
+% Maximal term depth : 2 ( 1 average)
+% Arithmetic symbols : 12 ( 0 pred; 0 func; 12 numbers)
+% SPC : CNF_SAT_RFO_EQU_NUE
+
+% Comments :
+% Bugfixes : v4.0.1 - Added more numbers, particularly rationals.
+% : v4.1.1 - Removed rationals with negative denominators.
+%------------------------------------------------------------------------------
+%----Quoted symbols
+cnf(distinct_object,axiom,
+ ( "An Apple" != "A \"Microsoft \\ escape\"" )).
+
+%----Numbers
+cnf(integers,axiom,
+ ( p(12)
+ | p(-12) )).
+
+cnf(rationals,axiom,
+ ( p(123/456)
+ | p(-123/456)
+ | p(+123/456) )).
+
+cnf(reals,axiom,
+ ( p(123.456 )
+ | p(-123.456 )
+ | p(123.456E789 )
+ | p(123.456e789 )
+ | p(-123.456E789 )
+ | p(123.456E-789 )
+ | p(-123.456E-789 ) )).
+
+%----Roles - seen axiom already
+cnf(role_definition,definition,
+ f(d) = f(X) ).
+
+cnf(role_assumption,assumption,
+ p(a) ).
+
+cnf(role_lemma,lemma,
+ p(l) ).
+
+cnf(role_theorem,theorem,
+ p(t) ).
+
+cnf(role_unknown,unknown,
+ p(u) ).
+
+%----Selective include directive
+include('Axioms/SYN000-0.ax',[ia1,ia3]).
+
+%----Source
+cnf(source_unknown,axiom,
+ p(X),
+ unknown).
+
+cnf(source,axiom,
+ p(X),
+ file('SYN000-1.p')).
+
+cnf(source_name,axiom,
+ p(X),
+ file('SYN000-1.p',source_unknown)).
+
+cnf(source_copy,axiom,
+ p(X),
+ source_unknown).
+
+cnf(source_introduced_assumption,axiom,
+ p(X),
+ introduced(assumption,[from,the,world])).
+
+cnf(source_inference,plain,
+ p(a),
+ inference(magic,
+ [status(thm),assumptions([source_introduced_assumption])],
+ [theory(equality),source_unknown]) ).
+
+cnf(source_inference_with_bind,plain,
+ p(a),
+ inference(magic,
+ [status(thm)],
+ [theory(equality),source_unknown:[bind(X,$fot(a))]]) ).
+
+%----Useful info
+cnf(useful_info,axiom,
+ p(X),
+ unknown,
+ [simple,
+ prolog(like,Data,[nested,12.2]),
+ AVariable,
+ 12.2,
+ "A distinct object",
+ $cnf(p(X) | ~q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b))))),
+ data(name):[colon,list,2],
+ [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]
+ ]).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000=2 : TPTP v5.5.0. Bugfixed v5.5.1.
+% Domain : Syntactic
+% Problem : TF0 syntax with arithmetic
+% Version : Biased.
+% English :
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Theorem
+% Rating : ? v5.5.1
+% Syntax : Number of formulae : 83 ( 73 unit; 6 type)
+% Number of atoms : 100 ( 4 equality)
+% Maximal formula depth : 7 ( 1 average)
+% Number of connectives : 14 ( 0 ~; 10 |; 1 &)
+% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
+% ( 0 ~|; 0 ~&)
+% Number of type conns : 3 ( 3 >; 0 *; 0 +; 0 <<)
+% Number of predicates : 20 ( 10 propositional; 0-2 arity)
+% Number of functors : 41 ( 24 constant; 0-2 arity)
+% Number of variables : 14 ( 1 sgn; 3 !; 11 ?)
+% Maximal term depth : 3 ( 1 average)
+% Arithmetic symbols : 37 ( 9 pred; 7 func; 21 numbers)
+% SPC : TF0_THM_EQU_ARI
+
+% Comments :
+% Bugfixes : v5.5.1 - Removed $evaleq.
+%------------------------------------------------------------------------------
+%----Types for what follows
+tff(p_int_type,type,(
+ p_int: $int > $o )).
+
+tff(p_rat_type,type,(
+ p_rat: $rat > $o )).
+
+tff(p_real_type,type,(
+ p_real: $real > $o )).
+
+tff(a_int,type,(
+ a_int: $int )).
+
+tff(a_rat,type,(
+ a_rat: $rat )).
+
+tff(a_real,type,(
+ a_real: $real )).
+
+%----Numbers
+tff(integers,axiom,
+ ( p_int(123)
+ | p_int(-123) )).
+
+tff(rationals,axiom,
+ ( p_rat(123/456)
+ | p_rat(-123/456)
+ | p_rat(123/456) )).
+
+tff(reals,axiom,
+ ( p_real(123.456)
+ | p_real(-123.456)
+ | p_real(123.456E78)
+ | p_real(123.456e78)
+ | p_real(-123.456E78)
+ | p_real(123.456E-78)
+ | p_real(-123.456E-78) )).
+
+%----Variables
+tff(variables_int,axiom,(
+ ! [X: $int] :
+ ? [Y: $int] :
+ ( p_int(X)
+ => p_int(Y) ) )).
+
+tff(variables_rat,axiom,(
+ ! [X: $rat] :
+ ? [Y: $rat] :
+ ( p_rat(X)
+ => p_rat(Y) ) )).
+
+tff(variables_real,axiom,(
+ ! [X: $real] :
+ ? [Y: $real] :
+ ( p_real(X)
+ => p_real(Y) ) )).
+
+%----Arithmetic relations
+tff(less_int,axiom,(
+ $less(a_int,3) )).
+
+tff(less_rat,axiom,(
+ $less(a_rat,3/9) )).
+
+tff(less_real,axiom,(
+ $less(a_real,3.3) )).
+
+tff(lesseq_int,axiom,(
+ $lesseq(a_int,3) )).
+
+tff(lesseq_rat,axiom,(
+ $lesseq(a_rat,3/9) )).
+
+tff(lesseq_real,axiom,(
+ $lesseq(a_real,3.3) )).
+
+tff(greater_int,axiom,(
+ $greater(a_int,-3) )).
+
+tff(greater_rat,axiom,(
+ $greater(a_rat,-3/9) )).
+
+tff(greater_real,axiom,(
+ $greater(a_real,-3.3) )).
+
+tff(greatereq_int,axiom,(
+ $greatereq(a_int,-3) )).
+
+tff(greatereq_rat,axiom,(
+ $greatereq(a_rat,-3/9) )).
+
+tff(greatereq_real,axiom,(
+ $greatereq(a_real,-3.3) )).
+
+tff(equal_int,axiom,(
+ a_int = 0 )).
+
+tff(equal_rat,axiom,(
+ a_rat = 0/1 )).
+
+tff(equal_real,axiom,(
+ a_real = 0.0 )).
+
+%----Arithmetic functions
+tff(uminus_int,axiom,(
+ p_int($uminus(3)) )).
+
+tff(uminus_rat,axiom,(
+ p_rat($uminus(3/9)) )).
+
+tff(uminus_real,axiom,(
+ p_real($uminus(3.3)) )).
+
+tff(sum_int,axiom,(
+ p_int($sum(3,3)) )).
+
+tff(sum_rat,axiom,(
+ p_rat($sum(3/9,3/9)) )).
+
+tff(sum_real,axiom,(
+ p_real($sum(3.3,3.3)) )).
+
+tff(difference_int,axiom,(
+ p_int($difference(3,3)) )).
+
+tff(difference_rat,axiom,(
+ p_rat($difference(3/9,3/9)) )).
+
+tff(difference_real,axiom,(
+ p_real($difference(3.3,3.3)) )).
+
+tff(product_int,axiom,(
+ p_int($product(3,3)) )).
+
+tff(product_rat,axiom,(
+ p_rat($product(3/9,3/9)) )).
+
+tff(product_real,axiom,(
+ p_real($product(3.3,3.3)) )).
+
+tff(quotient_rat,axiom,(
+ p_rat($quotient(3/9,3/9)) )).
+
+tff(quotient_real,axiom,(
+ p_real($quotient(3.3,3.3)) )).
+
+tff(quotient_e_int,axiom,(
+ p_int($quotient_e(3,3)) )).
+
+tff(quotient_e_rat,axiom,(
+ p_rat($quotient_e(3/9,3/9)) )).
+
+tff(quotient_e_real,axiom,(
+ p_real($quotient_e(3.3,3.3)) )).
+
+tff(quotient_t_int,axiom,(
+ p_int($quotient_t(3,3)) )).
+
+tff(quotient_t_rat,axiom,(
+ p_rat($quotient_t(3/9,3/9)) )).
+
+tff(quotient_t_real,axiom,(
+ p_real($quotient_t(3.3,3.3)) )).
+
+tff(quotient_f_int,axiom,(
+ p_int($quotient_f(3,3)) )).
+
+tff(quotient_f_rat,axiom,(
+ p_rat($quotient_f(3/9,3/9)) )).
+
+tff(quotient_f_real,axiom,(
+ p_real($quotient_f(3.3,3.3)) )).
+
+tff(remainder_e_int,axiom,(
+ p_int($remainder_e(3,3)) )).
+
+tff(remainder_e_rat,axiom,(
+ p_rat($remainder_e(3/9,3/9)) )).
+
+tff(remainder_e_real,axiom,(
+ p_real($remainder_e(3.3,3.3)) )).
+
+tff(remainder_t_int,axiom,(
+ p_int($remainder_t(3,3)) )).
+
+tff(remainder_t_rat,axiom,(
+ p_rat($remainder_t(3/9,3/9)) )).
+
+tff(remainder_t_real,axiom,(
+ p_real($remainder_t(3.3,3.3)) )).
+
+tff(remainder_f_int,axiom,(
+ p_int($remainder_f(3,3)) )).
+
+tff(remainder_f_rat,axiom,(
+ p_rat($remainder_f(3/9,3/9)) )).
+
+tff(remainder_f_real,axiom,(
+ p_real($remainder_f(3.3,3.3)) )).
+
+tff(floor_int,axiom,(
+ p_int($floor(3)) )).
+
+tff(floor_rat,axiom,(
+ p_rat($floor(3/9)) )).
+
+tff(floor_int,axiom,(
+ p_real($floor(3.3)) )).
+
+tff(ceiling_int,axiom,(
+ p_int($ceiling(3)) )).
+
+tff(ceiling_rat,axiom,(
+ p_rat($ceiling(3/9)) )).
+
+tff(ceiling_int,axiom,(
+ p_real($ceiling(3.3)) )).
+
+tff(truncate_int,axiom,(
+ p_int($truncate(3)) )).
+
+tff(truncate_rat,axiom,(
+ p_rat($truncate(3/9)) )).
+
+tff(truncate_int,axiom,(
+ p_real($truncate(3.3)) )).
+
+%----Recognizing numbers
+tff(is_int_int,axiom,(
+ ? [X: $int] : $is_int(X) )).
+
+tff(is_int_rat,axiom,(
+ ? [X: $rat] : $is_int(X) )).
+
+tff(is_int_real,axiom,(
+ ? [X: $real] : $is_int(X) )).
+
+tff(is_rat_rat,axiom,(
+ ? [X: $rat] : $is_rat(X) )).
+
+tff(is_rat_real,axiom,(
+ ? [X: $real] : $is_rat(X) )).
+
+%----Coercion
+tff(to_int_int,axiom,(
+ p_int($to_int(3)) )).
+
+tff(to_int_rat,axiom,(
+ p_int($to_int(3/9)) )).
+
+tff(to_int_real,axiom,(
+ p_int($to_int(3.3)) )).
+
+tff(to_rat_int,axiom,(
+ p_rat($to_rat(3)) )).
+
+tff(to_rat_rat,axiom,(
+ p_rat($to_rat(3/9)) )).
+
+tff(to_rat_real,axiom,(
+ p_rat($to_rat(3.3)) )).
+
+tff(to_real_int,axiom,(
+ p_real($to_real(3)) )).
+
+tff(to_real_rat,axiom,(
+ p_real($to_real(3/9)) )).
+
+tff(to_real_real,axiom,(
+ p_real($to_real(3.3)) )).
+
+%----A conjecture to prove
+tff(mixed,conjecture,(
+ ? [X: $int,Y: $rat,Z: $real] :
+ ( Y = $to_rat($sum(X,2))
+ & ( $less($to_int(Y),3)
+ | $greater($to_real(Y),3.3) ) ) )).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000_1 : TPTP v5.5.0. Released v5.0.0.
+% Domain : Syntactic
+% Problem : Basic TPTP TFF syntax without arithmetic
+% Version : Biased.
+% English : Basic TPTP TFF syntax that you can't survive without parsing.
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Theorem
+% Rating : 0.40 v5.5.0, 0.25 v5.4.0, 0.33 v5.2.0, 0.67 v5.0.0
+% Syntax : Number of formulae : 38 ( 21 unit; 25 type)
+% Number of atoms : 74 ( 3 equality)
+% Maximal formula depth : 7 ( 3 average)
+% Number of connectives : 28 ( 9 ~; 10 |; 3 &)
+% ( 1 <=>; 3 =>; 1 <=; 1 <~>)
+% ( 0 ~|; 0 ~&)
+% Number of type conns : 17 ( 10 >; 7 *; 0 +; 0 <<)
+% Number of predicates : 37 ( 30 propositional; 0-3 arity)
+% Number of functors : 10 ( 6 constant; 0-3 arity)
+% Number of variables : 14 ( 1 sgn; 6 !; 8 ?)
+% Maximal term depth : 4 ( 2 average)
+% SPC : TFF_THM_EQU_NAR
+
+% Comments :
+%------------------------------------------------------------------------------
+%----Propositional
+tff(p0_type,type,(
+ p0: $o )).
+
+tff(q0_type,type,(
+ q0: $o )).
+
+tff(r0_type,type,(
+ r0: $o )).
+
+tff(s0_type,type,(
+ s0: $o )).
+
+tff(propositional,axiom,
+ ( ( p0
+ & ~ q0 )
+ => ( r0
+ | ~ s0 ) )).
+
+%----First-order
+tff(a_type,type,(
+ a: $i )).
+
+tff(b_type,type,(
+ b: $i )).
+
+tff(h_type,type,(
+ h: $i )).
+
+tff(f_type,type,(
+ f: $i > $i )).
+
+tff(g_type,type,(
+ g: ( $i * $i * $i ) > $i )).
+
+tff(p_type,type,(
+ p: $i > $o )).
+
+tff(q_type,type,(
+ q: ( $i * $i ) > $o )).
+
+tff(r_type,type,(
+ r: ( $i * $i * $i ) > $o )).
+
+tff(s_type,type,(
+ s: $i > $o )).
+
+tff(first_order,axiom,(
+ ! [X: $i] :
+ ( ( p(X)
+ | ~ q(X,a) )
+ => ? [Y: $i,Z: $i] :
+ ( r(X,f(Y),g(X,f(Y),Z))
+ & ~ s(f(f(f(b)))) ) ) )).
+
+%----Equality
+tff(equality,axiom,(
+ ? [Y: $i] :
+ ! [X: $i,Z: $i] :
+ ( f(Y) = g(X,f(Y),Z)
+ | f(f(f(b))) != a
+ | X = f(Y) ) )).
+
+%----True and false
+tff(true_false,axiom,
+ ( $true
+ | $false )).
+
+tff(quoted_proposition_type,type,(
+ 'A proposition': $o )).
+
+tff(quoted_predicate_type,type,(
+ 'A predicate': $i > $o )).
+
+tff(quoted_constant_type,type,(
+ 'A constant': $i )).
+
+tff(quoted_function_type,type,(
+ 'A function': $i > $i )).
+
+tff(quoted_escape_type,type,(
+ 'A \'quoted \\ escape\'': $i )).
+
+%----Quoted symbols
+tff(single_quoted,axiom,
+ ( 'A proposition'
+ | 'A predicate'(a)
+ | p('A constant')
+ | p('A function'(a))
+ | p('A \'quoted \\ escape\'') )).
+
+%----Connectives - seen |, &, =>, ~ already
+tff(useful_connectives,axiom,(
+ ! [X: $i] :
+ ( ( p(X)
+ <= ~ q(X,a) )
+ <=> ? [Y: $i,Z: $i] :
+ ( r(X,f(Y),g(X,f(Y),Z))
+ <~> ~ s(f(f(f(b)))) ) ) )).
+
+%----New types
+tff(new_type,type,(
+ new: $tType )).
+
+tff(newc_type,type,(
+ newc: new )).
+
+tff(newf_type,type,(
+ newf: ( new * $i ) > new )).
+
+tff(newp_type,type,(
+ newp: ( new * $i ) > $o )).
+
+tff(new_axiom,axiom,(
+ ! [X: new] : newp(newf(newc,a),a) )).
+
+%----Annotated formula names
+tff(123,axiom,(
+ ! [X: $i] :
+ ( ( p(X)
+ | ~ q(X,a) )
+ => ? [Y: $i,Z: $i] :
+ ( r(X,f(Y),g(X,f(Y),Z))
+ & ~ s(f(f(f(b)))) ) ) )).
+
+%----Roles
+tff(role_hypothesis,hypothesis,(
+ p(h) )).
+
+tff(role_conjecture,conjecture,(
+ ? [X: $i] : p(X) )).
+
+%----Include directive
+include('Axioms/SYN000_0.ax').
+
+%----Comments
+/* This
+ is a block
+ comment.
+*/
+
+%------------------------------------------------------------------------------
--- /dev/null
+%------------------------------------------------------------------------------
+% File : SYN000_2 : TPTP v5.5.0. Bugfixed v5.5.1.
+% Domain : Syntactic
+% Problem : Advanced TPTP TF0 syntax without arithmetic
+% Version : Biased.
+% English : Advanced TPTP TF0 syntax that you will encounter some time.
+
+% Refs :
+% Source : [TPTP]
+% Names :
+
+% Status : Satisfiable
+% Rating : ? v5.5.1
+% Syntax : Number of formulae : 26 ( 18 unit; 7 type)
+% Number of atoms : 42 ( 2 equality)
+% Maximal formula depth : 5 ( 2 average)
+% Number of connectives : 6 ( 2 ~; 0 |; 1 &)
+% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
+% ( 1 ~|; 1 ~&)
+% Number of type conns : 9 ( 5 >; 4 *; 0 +; 0 <<)
+% Number of predicates : 14 ( 11 propositional; 0-2 arity)
+% Number of functors : 6 ( 4 constant; 0-2 arity)
+% Number of variables : 18 ( 0 sgn; 13 !; 1 ?)
+% Maximal term depth : 2 ( 1 average)
+% SPC : TF0_SAT_EQU_NAR
+
+% Comments :
+% Bugfixes : v5.5.1 - Fixed let_binders.
+%------------------------------------------------------------------------------
+%----Quoted symbols
+tff(distinct_object,axiom,(
+ "An Apple" != "A \"Microsoft \\ escape\"" )).
+
+%----Types for stuff below
+tff(a_type,type,(
+ a: $i )).
+
+tff(b_type,type,(
+ b: $i )).
+
+tff(f_type,type,(
+ f: $i > $i )).
+
+tff(g_type,type,(
+ g: ( $i * $i ) > $i )).
+
+tff(h_type,type,(
+ h: ( $i * $i * $i ) > $i )).
+
+tff(p_type,type,(
+ p: $i > $o )).
+
+tff(q_type,type,(
+ q: ( $i * $i ) > $o )).
+
+%----Conditional constructs
+tff(conditionals,axiom,(
+ ! [Z: $i] :
+ $ite_f(
+ ? [X: $i] : p(X)
+ , ! [X: $i] : q(X,X)
+ , q(Z,$ite_t(! [X: $i] : p(X), f(a), f(Z))) ) )).
+
+%----Let binders
+tff(let_binders,axiom,(
+ ! [X: $i] :
+ $let_ff(
+ ! [Y1: $i,Y2: $i] :
+ ( q(Y1,Y2)
+ <=> p(Y1) )
+ , ( q($let_tt(! [Z1: $i] : f(Z1) = g(Z1,b), f(a)),X)
+ & p($let_ft(! [Y3: $i] : ! [Y4: $i] : ( q(Y3,Y4) <=> $ite_f(Y3 = Y4, q(a,a), q(Y3,Y4) ) ), $ite_t(q(b,b), f(a), f(X)))) ) ) )).
+
+%----Rare connectives
+tff(never_used_connectives,axiom,(
+ ! [X: $i] :
+ ( ( p(X)
+ ~| ~ q(X,a) )
+ ~& p(X) ) )).
+
+%----Roles
+tff(role_definition,definition,(
+ ! [X: $i] : f(a) = f(X) )).
+
+tff(role_assumption,assumption,(
+ p(a) )).
+
+tff(role_lemma,lemma,(
+ p(a) )).
+
+tff(role_theorem,theorem,(
+ p(a) )).
+
+tff(role_unknown,unknown,(
+ p(a) )).
+
+%----Selective include directive
+include('Axioms/SYN000_0.ax',[ia1,ia3]).
+
+%----Source
+tff(source_unknown,axiom,(
+ ! [X: $i] : p(X) ),
+ unknown).
+
+tff(source,axiom,(
+ ! [X: $i] : p(X) ),
+ file('SYN000-1.p')).
+
+tff(source_name,axiom,(
+ ! [X: $i] : p(X) ),
+ file('SYN000-1.p',source_unknown)).
+
+tff(source_copy,axiom,(
+ ! [X: $i] : p(X) ),
+ source_unknown).
+
+tff(source_introduced_assumption,axiom,(
+ ! [X: $i] : p(X) ),
+ introduced(assumption,[from,the,world])).
+
+tff(source_inference,plain,(
+ p(a) ),
+ inference(magic,[status(thm),assumptions([source_introduced_assumption])],[theory(equality),source_unknown])).
+
+tff(source_inference_with_bind,plain,(
+ p(a) ),
+ inference(magic,[status(thm)],[theory(equality),source_unknown:[bind(X,$fot(a))]])).
+
+%----Useful info
+tff(useful_info,axiom,(
+ ! [X: $i] : p(X) ),
+ unknown,
+ [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2,"A distinct object",$tff(p(X) | ~ q(X,a)),data(name):[colon,list,2],[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]]).
+
+%------------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : SYN075+1 : TPTP v5.5.0. Released v2.0.0.
+% Domain : Syntactic
+% Problem : Pelletier Problem 52
+% Version : Especial.
+% English :
+
+% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
+% : [Hah94] Haehnle (1994), Email to G. Sutcliffe
+% Source : [Hah94]
+% Names : Pelletier 52 [Pel86]
+
+% Status : Theorem
+% Rating : 0.22 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.26 v5.2.0, 0.05 v5.0.0, 0.21 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.00 v3.3.0, 0.11 v3.2.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0
+% Syntax : Number of formulae : 2 ( 0 unit)
+% Number of atoms : 6 ( 4 equality)
+% Maximal formula depth : 7 ( 7 average)
+% Number of connectives : 4 ( 0 ~ ; 0 |; 1 &)
+% ( 3 <=>; 0 =>; 0 <=)
+% ( 0 <~>; 0 ~|; 0 ~&)
+% Number of predicates : 2 ( 0 propositional; 2-2 arity)
+% Number of functors : 0 ( 0 constant; --- arity)
+% Number of variables : 8 ( 0 singleton; 4 !; 4 ?)
+% Maximal term depth : 1 ( 1 average)
+% SPC : FOF_THM_RFO_SEQ
+
+% Comments :
+%--------------------------------------------------------------------------
+%----Problem axioms
+fof(pel52_1,axiom,
+ ( ? [Z,W] :
+ ! [X,Y] :
+ ( big_f(X,Y)
+ <=> ( X = Z
+ & Y = W ) ) )).
+
+fof(pel52,conjecture,
+ ( ? [W] :
+ ! [Y] :
+ ( ? [Z] :
+ ! [X] :
+ ( big_f(X,Y)
+ <=> X = Z )
+ <=> Y = W ) )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+%--------------------------------------------------------------------------
+% File : SYN075-1 : TPTP v5.5.0. Released v1.0.0.
+% Domain : Syntactic
+% Problem : Pelletier Problem 52
+% Version : Especial.
+% English :
+
+% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au
+% Source : [Pel86]
+% Names : Pelletier 52 [Pel86]
+
+% Status : Unsatisfiable
+% Rating : 0.00 v5.5.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.12 v5.1.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.08 v2.4.0, 0.11 v2.2.1, 0.11 v2.2.0, 0.22 v2.1.0, 0.33 v2.0.0
+% Syntax : Number of clauses : 10 ( 4 non-Horn; 0 unit; 8 RR)
+% Number of atoms : 31 ( 17 equality)
+% Maximal clause size : 4 ( 3 average)
+% Number of predicates : 2 ( 0 propositional; 2-2 arity)
+% Number of functors : 5 ( 2 constant; 0-2 arity)
+% Number of variables : 23 ( 2 singleton)
+% Maximal term depth : 2 ( 1 average)
+% SPC : CNF_UNS_RFO_SEQ_NHN
+
+% Comments :
+%--------------------------------------------------------------------------
+cnf(clause_1,axiom,
+ ( ~ big_f(X,Y)
+ | X = a )).
+
+cnf(clause_2,axiom,
+ ( ~ big_f(X,Y)
+ | Y = b )).
+
+cnf(clause_3,axiom,
+ ( X != a
+ | Y != b
+ | big_f(X,Y) )).
+
+cnf(clause_4,negated_conjecture,
+ ( ~ big_f(Y,f(X))
+ | Y != g(X)
+ | f(X) = X )).
+
+cnf(clause_5,negated_conjecture,
+ ( ~ big_f(Y,f(X))
+ | Y = g(X)
+ | big_f(h(X,Z),f(X))
+ | ~ big_f(h(X,Z),f(X)) )).
+
+cnf(clause_6,negated_conjecture,
+ ( Y != g(X)
+ | big_f(Y,f(X))
+ | f(X) = X )).
+
+cnf(clause_7,negated_conjecture,
+ ( Y != g(X)
+ | big_f(Y,f(X))
+ | big_f(h(X,Z),f(X))
+ | h(X,Z) = Z )).
+
+cnf(clause_8,negated_conjecture,
+ ( Y != g(X)
+ | big_f(Y,f(X))
+ | h(X,Z) != Z
+ | ~ big_f(h(X,Z),f(X)) )).
+
+cnf(clause_9,negated_conjecture,
+ ( f(X) != X
+ | big_f(h(X,Z),f(X))
+ | h(X,Z) = Z )).
+
+cnf(clause_10,negated_conjecture,
+ ( f(X) != X
+ | h(X,Z) != Z
+ | ~ big_f(h(X,Z),f(X)) )).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% example from the TFF0 paper
+% see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa
+%
+% Status : Theorem
+%
+tff(list_type,type, ( list: $tType )).
+tff(nil_type,type, ( nil: list )).
+tff(mycons_type,type,( mycons: ( $int * list ) > list )).
+tff(sorted_type,type,( fib_sorted: list > $o )).
+
+tff(empty_fib_sorted,axiom,(
+ fib_sorted(nil) )).
+tff(single_is_fib_sorted,axiom,(
+ ! [X: $int] : fib_sorted(mycons(X,nil)) )).
+tff(double_is_fib_sorted_if_ordered,axiom,(
+ ! [X: $int,Y: $int] :
+ ( $less(X,Y)
+ => fib_sorted(mycons(X,mycons(Y,nil))) ) )).
+tff(recursive_fib_sort,axiom,(
+ ! [X: $int,Y: $int,Z: $int,R: list] :
+ ( ( $less(X,Y)
+ & $greatereq(Z,$sum(X,Y))
+ & fib_sorted(mycons(Y,mycons(Z,R))) )
+ => fib_sorted(mycons(X,mycons(Y,mycons(Z,R)))) ) )).
+
+tff(check_list,conjecture,(
+ fib_sorted(mycons(1,mycons(2,mycons(4,nil)))) )).
--- /dev/null
+% example from the TFF0 paper
+% see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa
+%
+% Status : Theorem
+%
+tff(student_type,type, ( student: $tType )).
+tff(professor_type,type,( professor: $tType )).
+tff(course_type,type, ( course: $tType )).
+tff(michael_type,type, ( michael: student )).
+tff(victor_type,type, ( victor: professor )).
+tff(csc410_type,type, ( csc410: course )).
+tff(enrolled_type,type, ( enrolled: ( student * course ) > $o )).
+tff(teaches_type,type, ( teaches: ( professor * course ) > $o )).
+tff(taught_by_type,type,( taughtby: ( student * professor ) > $o )).
+tff(coordinator_of_type,type,( coordinatorof: course > professor )).
+
+tff(student_enrolled_axiom,axiom,(
+ ! [X: student] : ? [Y: course] : enrolled(X,Y) )).
+tff(professor_teaches,axiom,(
+ ! [X: professor] : ? [Y: course] : teaches(X,Y) )).
+tff(course_enrolled,axiom,(
+ ! [X: course] : ? [Y: student] : enrolled(Y,X) )).
+tff(course_teaches,axiom,(
+ ! [X: course] : ? [Y: professor] : teaches(Y,X) )).
+tff(coordinator_teaches,axiom,(
+ ! [X: course] : teaches(coordinatorof(X),X) )).
+tff(student_enrolled_taught,axiom,(
+ ! [X: student,Y: course] :
+ ( enrolled(X,Y)
+ => ! [Z: professor] : ( teaches(Z,Y) => taughtby(X,Z) ) ) )).
+tff(michael_enrolled_csc410_axiom,axiom,(
+ enrolled(michael,csc410) )).
+tff(victor_coordinator_csc410_axiom,axiom,(
+ coordinatorof(csc410) = victor )).
+
+tff(teaching_conjecture,conjecture,(
+ taughtby(michael,victor) )).
--- /dev/null
+% Status: Unsatisfiable
+
+%--------------------------------------------------------------------------
+
+/*
+cnf(query_1,axiom,
+ $false | $false /* | $false).
+*/
+
+cnf(query_1,axiom,
+ $false | $false | $false).
+
+cnf(query_1,negated_conjecture, ~
+ $false | $false | $false).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Theorem
+
+%--------------------------------------------------------------------------
+
+fof(query_1,axiom, ![A,B]: (A != B => e(A) != e(B)) ).
+
+fof(query_1,conjecture, e(1.6) != e(1) ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Unsatisfiable
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, a | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~a | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Unsatisfiable
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( a, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(a, d) | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Unsatisfiable
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, d) | ~ 'c' ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Satisfiable
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, e) | ~ 'c' ).
+
+cnf(query_1,axiom, e != d ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Satisfiable
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | cnf ).
+
+cnf(query_1,axiom, cnf | c ).
+
+cnf(query_1,axiom, ~p(A, axiom) | ~ 'c' ).
+
+cnf(query_1,axiom, axiom != d ).
+
+cnf(query_1,negated_conjecture, ~ cnf ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Satisfiable
+
+%--------------------------------------------------------------------------
+
+cnf(query_1,axiom, p( A, d ) | b ).
+
+cnf(query_1,axiom, b | c ).
+
+cnf(query_1,axiom, ~p(A, axiom) ).
+
+cnf(query_1,axiom, axiom != d ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: Satisfiable
+
+%--------------------------------------------------------------------------
+include('tptp_parser7.p').
+
+cnf(query_1,axiom, include('A') | b ).
+
+cnf(query_1,negated_conjecture, ~ b ).
+
+%--------------------------------------------------------------------------
--- /dev/null
+% Status: CounterSatisfiable
+
+%--------------------------------------------------------------------------
+
+fof(query_1,axiom, include(1) ).
+
+fof(query_1,axiom, ![E]: e(E,1.6) ).
+
+fof(query_1,axiom, ![A,E]: ~e(A,3.0E3) ).
+
+fof(query_1,conjecture, ![E]: e(E,2.6) ).
+
+%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unsat
-% EXIT: 20
-
-%--------------------------------------------------------------------------
-
-/*
-cnf(query_1,axiom,
- $false | $false /* | $false).
-*/
-
-cnf(query_1,axiom,
- $false | $false | $false).
-
-cnf(query_1,negated_conjecture, ~
- $false | $false | $false).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unsat
-% EXIT: 20
-
-%--------------------------------------------------------------------------
-
-fof(query_1,axiom, ![A,B]: (A != B => e(A) != e(B)) ).
-
-fof(query_1,conjecture, e(1.6) != e(1) ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unsat
-% EXIT: 20
-
-%--------------------------------------------------------------------------
-
-cnf(query_1,axiom, a | b ).
-
-cnf(query_1,axiom, b | c ).
-
-cnf(query_1,axiom, ~a | ~ 'c' ).
-
-cnf(query_1,negated_conjecture, ~ b ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unsat
-% EXIT: 20
-
-%--------------------------------------------------------------------------
-
-cnf(query_1,axiom, p( a, d ) | b ).
-
-cnf(query_1,axiom, b | c ).
-
-cnf(query_1,axiom, ~p(a, d) | ~ 'c' ).
-
-cnf(query_1,negated_conjecture, ~ b ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unsat
-% EXIT: 20
-
-%--------------------------------------------------------------------------
-
-cnf(query_1,axiom, p( A, d ) | b ).
-
-cnf(query_1,axiom, b | c ).
-
-cnf(query_1,axiom, ~p(A, d) | ~ 'c' ).
-
-cnf(query_1,negated_conjecture, ~ b ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unknown
-% EXIT: 0
-
-%--------------------------------------------------------------------------
-
-cnf(query_1,axiom, p( A, d ) | b ).
-
-cnf(query_1,axiom, b | c ).
-
-cnf(query_1,axiom, ~p(A, e) | ~ 'c' ).
-
-cnf(query_1,axiom, e != d ).
-
-cnf(query_1,negated_conjecture, ~ b ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unknown
-% EXIT: 0
-
-%--------------------------------------------------------------------------
-
-cnf(query_1,axiom, p( A, d ) | cnf ).
-
-cnf(query_1,axiom, cnf | c ).
-
-cnf(query_1,axiom, ~p(A, axiom) | ~ 'c' ).
-
-cnf(query_1,axiom, axiom != d ).
-
-cnf(query_1,negated_conjecture, ~ cnf ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unknown
-% EXIT: 0
-
-%--------------------------------------------------------------------------
-
-cnf(query_1,axiom, p( A, d ) | b ).
-
-cnf(query_1,axiom, b | c ).
-
-cnf(query_1,axiom, ~p(A, axiom) ).
-
-cnf(query_1,axiom, axiom != d ).
-
-cnf(query_1,negated_conjecture, ~ b ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unknown
-% EXIT: 0
-
-%--------------------------------------------------------------------------
-include('tptp_parser7.p').
-
-cnf(query_1,axiom, include('A') | b ).
-
-cnf(query_1,negated_conjecture, ~ b ).
-
-%--------------------------------------------------------------------------
+++ /dev/null
-% EXPECT: unknown
-% EXIT: 0
-
-%--------------------------------------------------------------------------
-
-fof(query_1,axiom, include(1) ).
-
-fof(query_1,axiom, ![E]: e(E,1.6) ).
-
-fof(query_1,axiom, ![A,E]: ~e(A,3.0E3) ).
-
-fof(query_1,conjecture, ![E]: e(E,2.6) ).
-
-%--------------------------------------------------------------------------
fi
command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
elif expr "$benchmark" : '.*\.p$' &>/dev/null; then
- proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1;
+ proof_command=PROOFS-NOT-SUPPORTED-IN-TPTP;
lang=tptp
+ command_line=--finite-model-find
expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes`
expected_output=$(grep '^% EXPECT: ' "$benchmark")
expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
if [ -z "$expected_output" -a -z "$expected_error" ]; then
- error "cannot determine expected output of \`$benchmark': " \
- "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
+ if grep -q '^% Status *: ' "$benchmark"; then
+ expected_output="$(grep '^% *Status *: ' "$benchmark" | head -1 | awk '{print$NF}')"
+ case "$expected_output" in
+ Theorem|Unsatisfiable) expected_exit_status=20 ;;
+ CounterSatisfiable|Satisfiable) expected_exit_status=10 ;;
+ GaveUp) expected_exit_status=0 ;;
+ esac
+ expected_output="% SZS status $expected_output for $(basename "$benchmark" | sed 's,\.p$,,')"
+ else
+ error "cannot determine expected output of \`$benchmark': " \
+ "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
+ fi
+ else
+ expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,')
+ expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
fi
- expected_output=$(echo "$expected_output" | perl -pe 's,^% EXPECT: ,,;s,\r,,')
- expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'`
if [ -z "$expected_exit_status" ]; then
error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
fi
- command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
+ if grep -q '^% COMMAND-LINE: ' "$benchmark"; then
+ command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'`
+ fi
else
error "benchmark \`$benchmark' must be *.cvc or *.smt or *.smt2 or *.p"
fi
projects / cvc5.git / commitdiff