diff options
79 files changed, 3577 insertions, 364 deletions
@@ -4,7 +4,10 @@ Changes since 1.2 ================= * 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 diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 524bc2095..3a2feb624 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -304,8 +304,8 @@ Expr ExprManager::mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherC 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 " @@ -323,8 +323,8 @@ Expr ExprManager::mkExpr(Expr opExpr) { 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 " @@ -342,8 +342,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { 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 " @@ -363,8 +363,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { 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 " @@ -386,8 +386,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) { 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 " @@ -410,8 +410,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, 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 " @@ -434,8 +434,8 @@ Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, 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 " diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 22d7baac3..8486e8ec3 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -126,18 +126,6 @@ ${metakind_kinds} 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 { @@ -324,9 +312,29 @@ ${metakind_ubchildren} } }/* 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 { diff --git a/src/expr/node.h b/src/expr/node.h index d9e88d8af..99e1e7ee7 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -1337,7 +1337,11 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, 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(); diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 1f098b4e8..64080c275 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -660,6 +660,9 @@ public: 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(); @@ -980,7 +983,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { #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(), @@ -1165,7 +1168,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { #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(), diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 0c62d31c5..913b8befb 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -353,6 +353,9 @@ public: 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. */ @@ -1280,6 +1283,10 @@ inline TypeNode NodeManager::mkSortConstructor(const std::string& name, 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; @@ -1367,80 +1374,114 @@ inline Node* NodeManager::mkNodePtr(Kind kind, // 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(); } @@ -1449,8 +1490,10 @@ template <bool ref_count> 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(); } @@ -1459,8 +1502,10 @@ template <bool ref_count> 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(); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 71c25bd50..f3cf992ba 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -317,6 +317,10 @@ bool Type::isSubrange() const { 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; diff --git a/src/expr/type.h b/src/expr/type.h index 5e4e86264..3c772d461 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -415,6 +415,9 @@ public: /** 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; diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 556e51216..9ee896107 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -24,11 +24,12 @@ 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) @@ -58,7 +59,7 @@ bool CommandExecutor::doCommand(Command* cmd) } } -bool CommandExecutor::doCommandSingleton(Command *cmd) +bool CommandExecutor::doCommandSingleton(Command* cmd) { bool status = true; if(d_options[options::verbosity] >= -1) { @@ -66,25 +67,27 @@ bool CommandExecutor::doCommandSingleton(Command *cmd) } 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) { diff --git a/src/main/command_executor.h b/src/main/command_executor.h index f1b8d8f2f..cbc71b075 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -34,6 +34,7 @@ protected: SmtEngine d_smtEngine; Options& d_options; StatisticsRegistry d_stats; + Result d_result; public: CommandExecutor(ExprManager &exprMgr, Options &options); @@ -47,7 +48,7 @@ public: */ bool doCommand(CVC4::Command* cmd); - virtual std::string getSmtEngineStatus(); + Result getResult() const { return d_result; } StatisticsRegistry& getStatisticsRegistry() { return d_stats; diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 63f689d48..2dfd5e6bd 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -184,7 +184,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // 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 || @@ -298,6 +298,16 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) 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); @@ -340,11 +350,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) }/* 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) { diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index f57d4f2d7..20a989106 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -297,13 +297,13 @@ int runCvc4(int argc, char* argv[], Options& opts) { 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; diff --git a/src/parser/options b/src/parser/options index e16f963f4..f277b231d 100644 --- a/src/parser/options +++ b/src/parser/options @@ -14,9 +14,6 @@ option memoryMap --mmap bool 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 diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 684a495b6..cb8c0d4f6 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -90,11 +90,7 @@ Parser* ParserBuilder::build() 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); @@ -152,7 +148,6 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) { } ParserBuilder& ParserBuilder::withOptions(const Options& options) { - d_szsCompliant = options[options::szsCompliant]; return withInputLanguage(options[options::inputLanguage]) .withMmap(options[options::memoryMap]) diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 9779bf37b..b6e15b2ff 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -80,9 +80,6 @@ class CVC4_PUBLIC ParserBuilder { /** 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); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 16b5bc4ea..c048feea7 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -786,7 +786,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] 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 */ diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 9e814b358..beeca818e 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -27,7 +27,7 @@ options { // 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 { @@ -102,6 +102,8 @@ using namespace CVC4::parser; #include "util/output.h" #include "util/rational.h" #include <vector> +#include <iterator> +#include <algorithm> using namespace CVC4; using namespace CVC4::parser; @@ -114,12 +116,12 @@ 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 */ /** @@ -139,46 +141,81 @@ parseCommand returns [CVC4::Command* cmd = NULL] @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); @@ -204,33 +241,30 @@ formulaRole[CVC4::parser::Tptp::FormulaRole & role] /* 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] @@ -241,28 +275,32 @@ 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 $$. @@ -270,35 +308,170 @@ definedProp[CVC4::Expr& expr] : 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; } @@ -308,19 +481,19 @@ plainTerm[CVC4::Expr& expr] } ; -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); @@ -331,18 +504,18 @@ variable[CVC4::Expr & expr] /*******/ /* 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; @@ -364,21 +537,21 @@ fofLogicFormula[CVC4::Expr & expr] } } ) - | //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; } @@ -389,20 +562,20 @@ fofUnitaryFormula[CVC4::Expr & expr] 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; } @@ -411,11 +584,229 @@ fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na] | 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 */ @@ -447,6 +838,7 @@ anything | FOF_TOK | THF_TOK | TFF_TOK + | TYPE_TOK | INCLUDE_TOK | DISTINCT_OBJECT | UPPER_WORD @@ -467,6 +859,8 @@ LBRACK_TOK : '['; RBRACK_TOK : ']'; COLON_TOK : ':'; +GREATER_TOK : '>'; + //operator OR_TOK : '|'; NOT_TOK : '~'; @@ -494,6 +888,7 @@ CNF_TOK : 'cnf'; 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 @@ -533,30 +928,30 @@ UPPER_WORD : UPPER_ALPHA ALPHA_NUMERIC*; 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 @@ -565,35 +960,34 @@ atomicWord[std::string & name] /* 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 @@ -601,26 +995,25 @@ NUMBER /* 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 */ @@ -629,5 +1022,3 @@ COMMENT | '/*' ( options {greedy=false;} : . )* '*/' { SKIP(); } //comment block ; - - diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 93c2168b1..3e6aa82b7 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -33,26 +33,26 @@ Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn /* 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) { @@ -92,7 +92,7 @@ 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. @@ -103,7 +103,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){ #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; } @@ -126,8 +126,15 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){ 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."); @@ -136,36 +143,78 @@ void Tptp::includeFile(std::string fileName){ // 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 */ diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index cea246282..79092e98f 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -25,6 +25,7 @@ #include <ext/hash_set> #include <cassert> #include "parser/options.h" +#include "parser/antlr_input.h" namespace CVC4 { @@ -46,51 +47,57 @@ class Tptp : public Parser { 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; } @@ -104,12 +111,13 @@ public: 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, @@ -126,8 +134,9 @@ public: 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); @@ -140,10 +149,30 @@ public: */ 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 */ @@ -153,48 +182,57 @@ public: 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: diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp index 34a620187..bfaeb07c9 100644 --- a/src/parser/tptp/tptp_input.cpp +++ b/src/parser/tptp/tptp_input.cpp @@ -28,9 +28,9 @@ 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 ); diff --git a/src/printer/Makefile.am b/src/printer/Makefile.am index fd48b8352..cd938088e 100644 --- a/src/printer/Makefile.am +++ b/src/printer/Makefile.am @@ -19,7 +19,9 @@ libprinter_la_SOURCES = \ 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 diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 344cbfe8c..f9d7c2a38 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -20,6 +20,7 @@ #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" @@ -41,8 +42,8 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() { 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(); diff --git a/src/printer/printer.h b/src/printer/printer.h index 5198a6ef1..d3a9201ee 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -45,6 +45,11 @@ protected: /** 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() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 1ab364f0c..76856532f 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -696,7 +696,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c) } 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); diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp new file mode 100644 index 000000000..ec2a8758b --- /dev/null +++ b/src/printer/tptp/tptp_printer.cpp @@ -0,0 +1,83 @@ +/********************* */ +/*! \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 */ diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h new file mode 100644 index 000000000..a0f3de62b --- /dev/null +++ b/src/printer/tptp/tptp_printer.h @@ -0,0 +1,46 @@ +/********************* */ +/*! \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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4ee00161f..b72f52092 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1108,13 +1108,15 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) } // 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)) || @@ -1133,7 +1135,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) 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(); @@ -2568,7 +2570,7 @@ Result SmtEngine::check() { 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)) { @@ -2579,7 +2581,7 @@ Result SmtEngine::check() { 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)) { @@ -2600,13 +2602,13 @@ Result SmtEngine::check() { 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); } @@ -3427,7 +3429,9 @@ Model* SmtEngine::getModel() throw(ModalException) { "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) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a45fe3383..552f5cd67 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -234,6 +234,11 @@ class CVC4_PUBLIC SmtEngine { Result d_status; /** + * The name of the input (if any). + */ + std::string d_filename; + + /** * A private utility class to SmtEngine. */ smt::SmtEnginePrivate* d_private; diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index fca79aff0..6a6fb2e31 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -300,7 +300,12 @@ operator SEXPR 0: "a symbolic expression" 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 \ @@ -344,6 +349,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule 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 \ diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 4d62ce511..392e146ba 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -16,6 +16,7 @@ **/ #include "theory/builtin/theory_builtin_rewriter.h" +#include "util/chain.h" using namespace std; @@ -53,7 +54,7 @@ Node TheoryBuiltinRewriter::blastChain(TNode in) { 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 diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2a4e07528..a04f9f88a 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -220,6 +220,14 @@ public: } };/* 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) { diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 51eb5cb1a..23318b95d 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -77,6 +77,7 @@ libutil_la_SOURCES = \ ite_removal.h \ ite_removal.cpp \ node_visitor.h \ + chain.h \ index.h \ uninterpreted_constant.h \ uninterpreted_constant.cpp \ @@ -139,7 +140,8 @@ EXTRA_DIST = \ rational.i \ hash.i \ predicate.i \ - uninterpreted_constant.i + uninterpreted_constant.i \ + chain.i DISTCLEANFILES = \ integer.h.tmp \ diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index e5c4ead6c..be39f69c1 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -22,6 +22,7 @@ #include <vector> #include <algorithm> +#include "expr/expr_manager_scope.h" #include "expr/node.h" #include "util/cvc4_assert.h" @@ -202,6 +203,7 @@ public: * @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(); } diff --git a/src/util/chain.h b/src/util/chain.h new file mode 100644 index 000000000..2e9cf7bf6 --- /dev/null +++ b/src/util/chain.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \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 */ diff --git a/src/util/chain.i b/src/util/chain.i new file mode 100644 index 000000000..1c97a527f --- /dev/null +++ b/src/util/chain.i @@ -0,0 +1,12 @@ +%{ +#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" diff --git a/src/util/result.cpp b/src/util/result.cpp index e0e34f07d..909a7d8c6 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -27,11 +27,12 @@ using namespace std; 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") { @@ -115,13 +116,13 @@ Result Result::asSatisfiabilityResult() const throw() { 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); @@ -129,7 +130,7 @@ Result Result::asSatisfiabilityResult() const throw() { } // TYPE_NONE - return Result(SAT_UNKNOWN, NO_STATUS); + return Result(SAT_UNKNOWN, NO_STATUS, d_inputName); } Result Result::asValidityResult() const throw() { @@ -141,13 +142,13 @@ 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); @@ -155,7 +156,7 @@ Result Result::asValidityResult() const throw() { } // TYPE_NONE - return Result(VALIDITY_UNKNOWN, NO_STATUS); + return Result(VALIDITY_UNKNOWN, NO_STATUS, d_inputName); } string Result::toString() const { diff --git a/src/util/result.h b/src/util/result.h index cb1bd50fa..54ec3a38c 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -71,47 +71,58 @@ private: 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; @@ -142,6 +153,8 @@ public: std::string toString() const; + std::string getInputName() const { return d_inputName; } + };/* class Result */ inline bool Result::operator!=(const Result& r) const throw() { diff --git a/src/util/util_model.h b/src/util/util_model.h index 365e7124d..e5bd1f955 100644 --- a/src/util/util_model.h +++ b/src/util/util_model.h @@ -33,6 +33,10 @@ std::ostream& operator<<(std::ostream&, const Model&); 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 */ @@ -52,6 +56,8 @@ public: 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 */ diff --git a/test/Makefile.am b/test/Makefile.am index 0fdc69e03..1ac00eb82 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -51,6 +51,7 @@ subdirs_to_check = \ regress/regress0/push-pop/boolean \ regress/regress0/precedence \ regress/regress0/preprocess \ + regress/regress0/tptp \ regress/regress0/unconstrained \ regress/regress0/decision \ regress/regress0/fmf \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index e380f2fc2..b1c15c73a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,5 +1,5 @@ -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 @@ -101,17 +101,7 @@ CVC_TESTS = \ 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 = \ diff --git a/test/regress/regress0/tptp/ARI086=1.p b/test/regress/regress0/tptp/ARI086=1.p new file mode 100644 index 000000000..f6d2fcb28 --- /dev/null +++ b/test/regress/regress0/tptp/ARI086=1.p @@ -0,0 +1,32 @@ +%------------------------------------------------------------------------------ +% 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 )). +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/Axioms/BOO004-0.ax b/test/regress/regress0/tptp/Axioms/BOO004-0.ax new file mode 100644 index 000000000..e02b4c2f8 --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/BOO004-0.ax @@ -0,0 +1,48 @@ +%-------------------------------------------------------------------------- +% 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 )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/Axioms/SYN000+0.ax b/test/regress/regress0/tptp/Axioms/SYN000+0.ax new file mode 100644 index 000000000..24ef682b7 --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/SYN000+0.ax @@ -0,0 +1,37 @@ +%------------------------------------------------------------------------------ +% 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). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/Axioms/SYN000-0.ax b/test/regress/regress0/tptp/Axioms/SYN000-0.ax new file mode 100644 index 000000000..d67e61aee --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/SYN000-0.ax @@ -0,0 +1,34 @@ +%------------------------------------------------------------------------------ +% 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). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/Axioms/SYN000_0.ax b/test/regress/regress0/tptp/Axioms/SYN000_0.ax new file mode 100644 index 000000000..acb557ef4 --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/SYN000_0.ax @@ -0,0 +1,47 @@ +%------------------------------------------------------------------------------ +% 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 )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/BOO003-4.p b/test/regress/regress0/tptp/BOO003-4.p new file mode 100644 index 000000000..0ea15fefc --- /dev/null +++ b/test/regress/regress0/tptp/BOO003-4.p @@ -0,0 +1,31 @@ +%-------------------------------------------------------------------------- +% 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 )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/BOO027-1.p b/test/regress/regress0/tptp/BOO027-1.p new file mode 100644 index 000000000..a3cd4224c --- /dev/null +++ b/test/regress/regress0/tptp/BOO027-1.p @@ -0,0 +1,48 @@ +%-------------------------------------------------------------------------- +% 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 )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p new file mode 100644 index 000000000..922a6cfc3 --- /dev/null +++ b/test/regress/regress0/tptp/DAT001=1.p @@ -0,0 +1,57 @@ +%------------------------------------------------------------------------------ +% 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)))))) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/KRS018+1.p b/test/regress/regress0/tptp/KRS018+1.p new file mode 100644 index 000000000..91039877b --- /dev/null +++ b/test/regress/regress0/tptp/KRS018+1.p @@ -0,0 +1,55 @@ +%------------------------------------------------------------------------------ +% 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) ) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/KRS063+1.p b/test/regress/regress0/tptp/KRS063+1.p new file mode 100644 index 000000000..737741dee --- /dev/null +++ b/test/regress/regress0/tptp/KRS063+1.p @@ -0,0 +1,181 @@ +%------------------------------------------------------------------------------ +% 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) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/MGT019+2.p b/test/regress/regress0/tptp/MGT019+2.p new file mode 100644 index 000000000..fb2cd7f62 --- /dev/null +++ b/test/regress/regress0/tptp/MGT019+2.p @@ -0,0 +1,84 @@ +%-------------------------------------------------------------------------- +% 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)) ) ) ) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/MGT031-1.p b/test/regress/regress0/tptp/MGT031-1.p new file mode 100644 index 000000000..f5cd1937e --- /dev/null +++ b/test/regress/regress0/tptp/MGT031-1.p @@ -0,0 +1,95 @@ +%-------------------------------------------------------------------------- +% 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) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/MGT041-2.p b/test/regress/regress0/tptp/MGT041-2.p new file mode 100644 index 000000000..a10a2f42d --- /dev/null +++ b/test/regress/regress0/tptp/MGT041-2.p @@ -0,0 +1,61 @@ +%-------------------------------------------------------------------------- +% 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) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/Makefile b/test/regress/regress0/tptp/Makefile new file mode 100644 index 000000000..8c3909592 --- /dev/null +++ b/test/regress/regress0/tptp/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/tptp + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am new file mode 100644 index 000000000..130a9dc7c --- /dev/null +++ b/test/regress/regress0/tptp/Makefile.am @@ -0,0 +1,79 @@ +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: diff --git a/test/regress/regress0/tptp/NLP114-1.p b/test/regress/regress0/tptp/NLP114-1.p new file mode 100644 index 000000000..cf5bd272a --- /dev/null +++ b/test/regress/regress0/tptp/NLP114-1.p @@ -0,0 +1,202 @@ +%-------------------------------------------------------------------------- +% 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 )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/PUZ131_1.p b/test/regress/regress0/tptp/PUZ131_1.p new file mode 100644 index 000000000..b9e1c648b --- /dev/null +++ b/test/regress/regress0/tptp/PUZ131_1.p @@ -0,0 +1,100 @@ +%------------------------------------------------------------------------------ +% 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) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000+1.p b/test/regress/regress0/tptp/SYN000+1.p new file mode 100644 index 000000000..682c11b69 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000+1.p @@ -0,0 +1,99 @@ +%------------------------------------------------------------------------------ +% 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. +*/ + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000+2.p b/test/regress/regress0/tptp/SYN000+2.p new file mode 100644 index 000000000..8c6f2f9f9 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000+2.p @@ -0,0 +1,127 @@ +%------------------------------------------------------------------------------ +% 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] + ]). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000-1.p b/test/regress/regress0/tptp/SYN000-1.p new file mode 100644 index 000000000..b6a68ec95 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000-1.p @@ -0,0 +1,83 @@ +%------------------------------------------------------------------------------ +% 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. +*/ + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000-2.p b/test/regress/regress0/tptp/SYN000-2.p new file mode 100644 index 000000000..0c6c0b59f --- /dev/null +++ b/test/regress/regress0/tptp/SYN000-2.p @@ -0,0 +1,117 @@ +%------------------------------------------------------------------------------ +% 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] + ]). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000=2.p b/test/regress/regress0/tptp/SYN000=2.p new file mode 100644 index 000000000..802613f4b --- /dev/null +++ b/test/regress/regress0/tptp/SYN000=2.p @@ -0,0 +1,309 @@ +%------------------------------------------------------------------------------ +% 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) ) ) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000_1.p b/test/regress/regress0/tptp/SYN000_1.p new file mode 100644 index 000000000..ed683c070 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000_1.p @@ -0,0 +1,170 @@ +%------------------------------------------------------------------------------ +% 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. +*/ + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000_2.p b/test/regress/regress0/tptp/SYN000_2.p new file mode 100644 index 000000000..ece5fa6b1 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000_2.p @@ -0,0 +1,135 @@ +%------------------------------------------------------------------------------ +% 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]]). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN075+1.p b/test/regress/regress0/tptp/SYN075+1.p new file mode 100644 index 000000000..7ef40217c --- /dev/null +++ b/test/regress/regress0/tptp/SYN075+1.p @@ -0,0 +1,46 @@ +%-------------------------------------------------------------------------- +% 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 ) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/SYN075-1.p b/test/regress/regress0/tptp/SYN075-1.p new file mode 100644 index 000000000..40b49fa36 --- /dev/null +++ b/test/regress/regress0/tptp/SYN075-1.p @@ -0,0 +1,76 @@ +%-------------------------------------------------------------------------- +% 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)) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/tff0-arith.p b/test/regress/regress0/tptp/tff0-arith.p new file mode 100644 index 000000000..c0e9af25a --- /dev/null +++ b/test/regress/regress0/tptp/tff0-arith.p @@ -0,0 +1,27 @@ +% 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)))) )). diff --git a/test/regress/regress0/tptp/tff0.p b/test/regress/regress0/tptp/tff0.p new file mode 100644 index 000000000..0402687bc --- /dev/null +++ b/test/regress/regress0/tptp/tff0.p @@ -0,0 +1,37 @@ +% 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) )). diff --git a/test/regress/regress0/tptp_parser.p b/test/regress/regress0/tptp/tptp_parser.p index 0be0adbbf..9c10d5bd3 100644 --- a/test/regress/regress0/tptp_parser.p +++ b/test/regress/regress0/tptp/tptp_parser.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser10.p b/test/regress/regress0/tptp/tptp_parser10.p index 90db619e7..d6a257121 100644 --- a/test/regress/regress0/tptp_parser10.p +++ b/test/regress/regress0/tptp/tptp_parser10.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Theorem %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser2.p b/test/regress/regress0/tptp/tptp_parser2.p index 83a5f7b83..e165b6b2f 100644 --- a/test/regress/regress0/tptp_parser2.p +++ b/test/regress/regress0/tptp/tptp_parser2.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser3.p b/test/regress/regress0/tptp/tptp_parser3.p index 3677e6ffe..2840892bc 100644 --- a/test/regress/regress0/tptp_parser3.p +++ b/test/regress/regress0/tptp/tptp_parser3.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser4.p b/test/regress/regress0/tptp/tptp_parser4.p index 6c5bd29da..448db77d2 100644 --- a/test/regress/regress0/tptp_parser4.p +++ b/test/regress/regress0/tptp/tptp_parser4.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser5.p b/test/regress/regress0/tptp/tptp_parser5.p index 23ddf3e60..c90d1cdad 100644 --- a/test/regress/regress0/tptp_parser5.p +++ b/test/regress/regress0/tptp/tptp_parser5.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser6.p b/test/regress/regress0/tptp/tptp_parser6.p index 799bc4c6d..6283eb29a 100644 --- a/test/regress/regress0/tptp_parser6.p +++ b/test/regress/regress0/tptp/tptp_parser6.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser7.p b/test/regress/regress0/tptp/tptp_parser7.p index f87c3484c..73c2b3834 100644 --- a/test/regress/regress0/tptp_parser7.p +++ b/test/regress/regress0/tptp/tptp_parser7.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser8.p b/test/regress/regress0/tptp/tptp_parser8.p index 4bb2694ea..da281151b 100644 --- a/test/regress/regress0/tptp_parser8.p +++ b/test/regress/regress0/tptp/tptp_parser8.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- include('tptp_parser7.p'). diff --git a/test/regress/regress0/tptp_parser9.p b/test/regress/regress0/tptp/tptp_parser9.p index bcbb88598..9bed19702 100644 --- a/test/regress/regress0/tptp_parser9.p +++ b/test/regress/regress0/tptp/tptp_parser9.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: CounterSatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/run_regression b/test/regress/run_regression index 084df6ac9..b740e8486 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -164,21 +164,35 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then 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 |