diff options
Diffstat (limited to 'src')
37 files changed, 1115 insertions, 325 deletions
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 */ |