diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 14:11:14 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-28 14:11:14 -0400 |
| commit | c28d0a243dbfd4295f785a017890251bd2670ce8 (patch) | |
| tree | 58b7c8ef04cc14563129017d9c2c8717f400825d | |
| parent | 6f6703473ccc66b3d2bdefed688602f93d33cd8f (diff) | |
| parent | ca423e291b1f7d67e1a325bb6d98663d6c0690c7 (diff) | |
Merge pull request #25 from kbansal/sets
Sets
37 files changed, 1261 insertions, 155 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 22c47da59..ecd3df084 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -304,26 +304,16 @@ TypeNode NodeManager::getType(TNode n, bool check) return typeNode; } -Node NodeManager::mkSkolem(const std::string& name, const TypeNode& type, const std::string& comment, int flags) { +Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) { Node n = NodeBuilder<0>(this, kind::SKOLEM); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); if((flags & SKOLEM_EXACT_NAME) == 0) { - size_t pos = name.find("$$"); - if(pos != string::npos) { - // replace a "$$" with the node ID - stringstream id; - id << n.getId(); - string newName = name; - newName.replace(pos, 2, id.str()); - setAttribute(n, expr::VarNameAttr(), newName); - } else { - stringstream newName; - newName << name << '_' << n.getId(); - setAttribute(n, expr::VarNameAttr(), newName.str()); - } + stringstream name; + name << prefix << '_' << n.getId(); + setAttribute(n, expr::VarNameAttr(), name.str()); } else { - setAttribute(n, expr::VarNameAttr(), name); + setAttribute(n, expr::VarNameAttr(), prefix); } if((flags & SKOLEM_NO_NOTIFY) == 0) { for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 15c49efd8..f533d3ab9 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -424,12 +424,11 @@ public: /** * Create a skolem constant with the given name, type, and comment. * - * @param name the name of the new skolem variable. This name can - * contain the special character sequence "$$", in which case the - * $$ is replaced with the Node ID. That way a family of skolem - * variables can be made with unique identifiers, used in dump, - * tracing, and debugging output. By convention, you should probably - * call mkSkolem() with a custom name appended with "_$$". + * @param prefix the name of the new skolem variable is the prefix + * appended with the Node ID. This way a family of skolem variables + * can be made with unique identifiers, used in dump, tracing, and + * debugging output. Use SKOLEM_EXECT_NAME flag if you don't want + * Node ID appended and use prefix as the name. * * @param type the type of the skolem variable to create * @@ -440,7 +439,7 @@ public: * @param flags an optional mask of bits from SkolemFlags to control * mkSkolem() behavior */ - Node mkSkolem(const std::string& name, const TypeNode& type, + Node mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment = "", int flags = SKOLEM_DEFAULT); /** Create a instantiation constant with the given type. */ diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index e4fcf6024..cfaa76aa8 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -30,12 +30,6 @@ vector<Options> parseThreadSpecificOptions(Options opts) unsigned numThreads = opts[options::threads]; - /** - * Use satRandomSeed for generating random numbers, in particular - * satRandomSeed-s - */ - srand(-opts[options::satRandomSeed]); - for(unsigned i = 0; i < numThreads; ++i) { threadOptions.push_back(opts); Options& tOpts = threadOptions.back(); @@ -43,11 +37,6 @@ vector<Options> parseThreadSpecificOptions(Options opts) // Set thread identifier tOpts.set(options::thread_id, i); - // If the random-seed is negative, pick a random seed randomly - if(opts[options::satRandomSeed] < 0) { - tOpts.set(options::satRandomSeed, unsigned(rand())); - } - if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) { diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index 2298f5880..3779f75c1 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -25,6 +25,7 @@ #include <sstream> #include "expr/command.h" +#include "util/didyoumean.h" #include "util/language.h" namespace CVC4 { @@ -99,11 +100,24 @@ inline InputLanguage stringToInputLanguage(std::string option, std::string optar Unreachable(); } +inline std::string suggestTags(char const* const* validTags, std::string inputTag) +{ + DidYouMean didYouMean; + + const char* opt; + for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) { + didYouMean.addWord(validTags[i]); + } + + return didYouMean.getMatchAsString(inputTag); +} + inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) { if(Configuration::isTracingBuild()) { if(!Configuration::isTraceTag(optarg.c_str())) throw OptionException(std::string("trace tag ") + optarg + - std::string(" not available")); + std::string(" not available.") + + suggestTags(Configuration::getTraceTags(), optarg) ); } else { throw OptionException("trace tags not available in non-tracing builds"); } @@ -115,7 +129,8 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt) if(!Configuration::isDebugTag(optarg.c_str()) && !Configuration::isTraceTag(optarg.c_str())) { throw OptionException(std::string("debug tag ") + optarg + - std::string(" not available")); + std::string(" not available.") + + suggestTags(Configuration::getDebugTags(), optarg) ); } } else if(! Configuration::isDebugBuild()) { throw OptionException("debug tags not available in non-debug builds"); diff --git a/src/options/options.h b/src/options/options.h index eaafade93..b41c9a66e 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -119,12 +119,11 @@ public: static void printLanguageHelp(std::ostream& out); /** - * Look up long command-line option names that bear some similarity to - * the given name. Don't include the initial "--". This might be - * useful in case of typos. Can return an empty vector if there are - * no suggestions. + * Look up long command-line option names that bear some similarity + * to the given name. Returns an empty string if there are no + * suggestions. */ - static std::vector<std::string> suggestCommandLineOptions(const std::string& optionName) throw(); + static std::string suggestCommandLineOptions(const std::string& optionName) throw(); /** * Look up SMT option names that bear some similarity to diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 02bfc6ca0..fc8b31d49 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Kshitij Bansal ** 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 @@ -47,13 +47,14 @@ extern int optreset; #include "expr/expr.h" #include "util/configuration.h" +#include "util/didyoumean.h" #include "util/exception.h" #include "util/language.h" #include "util/tls.h" ${include_all_option_headers} -#line 57 "${template}" +#line 58 "${template}" #include "util/output.h" #include "options/options_holder.h" @@ -62,7 +63,7 @@ ${include_all_option_headers} ${option_handler_includes} -#line 66 "${template}" +#line 67 "${template}" using namespace CVC4; using namespace CVC4::options; @@ -199,7 +200,7 @@ void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) { ${all_custom_handlers} -#line 203 "${template}" +#line 204 "${template}" #ifdef CVC4_DEBUG # define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true @@ -229,18 +230,18 @@ options::OptionsHolder::OptionsHolder() : ${all_modules_defaults} { } -#line 233 "${template}" +#line 234 "${template}" static const std::string mostCommonOptionsDescription = "\ Most commonly-used CVC4 options:${common_documentation}"; -#line 238 "${template}" +#line 239 "${template}" static const std::string optionsDescription = mostCommonOptionsDescription + "\n\ \n\ Additional CVC4 options:${remaining_documentation}"; -#line 244 "${template}" +#line 245 "${template}" static const std::string optionsFootnote = "\n\ [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ @@ -312,7 +313,7 @@ static struct option cmdlineOptions[] = {${all_modules_long_options} { NULL, no_argument, NULL, '\0' } };/* cmdlineOptions */ -#line 316 "${template}" +#line 317 "${template}" static void preemptGetopt(int& argc, char**& argv, const char* opt) { const size_t maxoptlen = 128; @@ -505,7 +506,7 @@ std::vector<std::string> Options::parseOptions(int argc, char* main_argv[]) thro switch(c) { ${all_modules_option_handlers} -#line 509 "${template}" +#line 510 "${template}" case ':': // This can be a long or short option, and the way to get at the @@ -549,7 +550,8 @@ ${all_modules_option_handlers} break; } - throw OptionException(std::string("can't understand option `") + option + "'"); + throw OptionException(std::string("can't understand option `") + option + "'" + + suggestCommandLineOptions(option)); } } @@ -558,22 +560,20 @@ ${all_modules_option_handlers} return nonOptions; } -std::vector<std::string> Options::suggestCommandLineOptions(const std::string& optionName) throw() { - std::vector<std::string> suggestions; +std::string Options::suggestCommandLineOptions(const std::string& optionName) throw() { + DidYouMean didYouMean; const char* opt; for(size_t i = 0; (opt = cmdlineOptions[i].name) != NULL; ++i) { - if(std::strstr(opt, optionName.c_str()) != NULL) { - suggestions.push_back(opt); - } + didYouMean.addWord(std::string("--") + cmdlineOptions[i].name); } - return suggestions; + return didYouMean.getMatchAsString(optionName); } static const char* smtOptions[] = { ${all_modules_smt_options}, -#line 577 "${template}" +#line 589 "${template}" NULL };/* smtOptions[] */ @@ -595,7 +595,7 @@ SExpr Options::getOptions() const throw() { ${all_modules_get_options} -#line 599 "${template}" +#line 611 "${template}" return SExpr(opts); } diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index d498d3c54..88b43eb0e 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Christopher L. Conway ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Francois Bobot + ** Minor contributors (to current version): Francois Bobot, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -284,20 +284,167 @@ void AntlrInput::warning(const std::string& message) { Warning() << getInputStream()->getName() << ':' << d_lexer->getLine(d_lexer) << '.' << d_lexer->getCharPositionInLine(d_lexer) << ": " << message << endl; } + +/** + * characters considered part of a simple symbol in SMTLIB. + * + * TODO: Ideally this code shouldn't be smtlib specific (should work + * with CVC language too), but this per-language specialization has + * been left for a later point. + */ +inline bool isSimpleChar(char ch) { + return isalnum(ch) || (strchr("~!@$%^&*_-+=<>.?/", ch) != NULL); +} + +/** + * Gets part of original input and tries to visually hint where the + * error might be. + * + * Something like: + * + * ...nd (= alpha beta) (= beta delta)) + * ^ + * + * Implementation (as on 2014/04/24): + * + * > if suggested pointer by lexer is under a "simple char", move to + * start of the word and print pointer there. + * + * > in the other case, it tries to find the nearest word in the error + * message passed along. if it can't find it, we don't add this + * visual hint, as experimentally position suggested by lexer was + * found to be totally unhelpful. (TODO: fix this upstream to + * improve) + */ +std::string parseErrorHelper(const char* lineStart, int charPositionInLine, const std::string& message) +{ + // Is it a multi-line message + bool multilineMessage = (message.find('\n') != string::npos); + // Useful only if it is a multi-line message + int firstLineEnd = message.find('\n'); + + std::ostringstream ss, slicess; + + // Keep first line of message + if(multilineMessage) { + ss << message.substr(0, firstLineEnd) << endl << endl; + } else { + ss << message << endl << endl; + } + + int posSliceStart = (charPositionInLine - 50 <= 0) ? 0 : charPositionInLine - 50 + 5; + int posSliceEnd = posSliceStart + 70; + int caretPos = 0; + int caretPosExtra = 0; // for inital intendation, epilipses etc. + + ss << " "; caretPosExtra += 2; + if(posSliceStart > 0) { + ss << "..."; caretPosExtra += 3; + } + + for(int i = posSliceStart; lineStart[i] != '\n'; ++i) { + if(i == posSliceEnd) { + ss << "..."; + break; + } + if(i < charPositionInLine) { caretPos++; } + + if(!isprint(lineStart[i])) { + // non-printable character, something wrong, bail out + return message; + } + + ss << (lineStart[i]); + slicess << (lineStart[i]); + } + + // adjust position of caret, based on slice and message + { + int caretPosOrig = caretPos; + string slice = slicess.str(); + if(isSimpleChar(slice[caretPos])) { + // if alphanumeric, try to go to beginning of word/number + while(caretPos > 0 && isSimpleChar(slice[caretPos - 1])) { --caretPos; } + if(caretPos == 0 && posSliceStart > 0) { + // reached start and this is not really the start? bail out + return message; + } else { + // likely it is also in original message? if so, very likely + // we found the right place + string word = slice.substr(caretPos, (caretPosOrig - caretPos + 1)); + int messagePosSt = message.find(word); + int messagePosEn = messagePosSt + (caretPosOrig - caretPos); + if( messagePosSt < string::npos && + (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) && + (messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) { + // ^the complicated if statement is just 'whole-word' match + Debug("friendlyparser") << "[friendlyparser] Feeling good." << std::endl; + } + } + } else { + // go to nearest alphanumeric string (before current position), + // see if that word can be found in original message. If so, + // point to that, else keep pointer where it was. + int nearestWordEn = caretPos - 1; + while(nearestWordEn > 0 && !isSimpleChar(slice[nearestWordEn])) { + --nearestWordEn; + } + if(isSimpleChar(slice[nearestWordEn])) { + int nearestWordSt = nearestWordEn; + while(nearestWordSt > 0 && isSimpleChar(slice[nearestWordSt - 1])) { + --nearestWordSt; + } + string word = slice.substr(nearestWordSt, (nearestWordEn - nearestWordSt + 1)); + Debug("friendlyparser") << "[friendlyparser] nearest word = " << word << std::endl; + int messagePosSt = message.find(word); + int messagePosEn = messagePosSt + (nearestWordEn - nearestWordSt + 1); + if( messagePosSt < string::npos && + (messagePosSt == 0 || !isSimpleChar(message[messagePosSt-1]) ) && + (messagePosEn+1 == message.size() || !isSimpleChar(message[messagePosEn+1]) ) ) { + // ^the complicated if statement is just 'whole-word' match + Debug("friendlyparser") << "[friendlyparser] strong evidence that caret should be at " + << nearestWordSt << std::endl; + caretPos = nearestWordSt; + } else { + // this doesn't look good. caret generally getting printed + // at unhelpful positions. improve upstream? + return message; + } + } + } + caretPos += caretPosExtra; + }// end of caret position computation/heuristics + + ss << std::endl; + while( caretPos-- > 0 ) { + ss << ' '; + } + ss << '^' << endl; + if(multilineMessage) { + ss << message.substr(firstLineEnd, message.size() - firstLineEnd);; + } + return ss.str(); +} + void AntlrInput::parseError(const std::string& message, bool eofException) throw (ParserException) { + + string updatedMessage = parseErrorHelper((const char*)d_antlr3InputStream->getLineBuf(d_antlr3InputStream), + d_lexer->getCharPositionInLine(d_lexer), + message); + Debug("parser") << "Throwing exception: " << (const char*)d_lexer->rec->state->tokSource->fileName->chars << ":" << d_lexer->getLine(d_lexer) << "." << d_lexer->getCharPositionInLine(d_lexer) << ": " - << message << endl; + << updatedMessage << endl; if(eofException) { throw ParserEndOfFileException(message, (const char*)d_lexer->rec->state->tokSource->fileName->chars, d_lexer->getLine(d_lexer), d_lexer->getCharPositionInLine(d_lexer)); } else { - throw ParserException(message, + throw ParserException(updatedMessage, (const char*)d_lexer->rec->state->tokSource->fileName->chars, d_lexer->getLine(d_lexer), d_lexer->getCharPositionInLine(d_lexer)); diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 4f182fb69..d5dcae726 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -418,7 +418,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){ Node cnd = findIteCnd(binor[0], binor[1]); - Node sk = nm->mkSkolem("deor$$", nm->booleanType()); + Node sk = nm->mkSkolem("deor", nm->booleanType()); Node ite = sk.iteNode(otherL, otherR); d_skolems.insert(sk, cnd); d_skolemsAdded.push_back(sk); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index a63de446c..0c8ca7507 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -226,7 +226,7 @@ Node TheoryArithPrivate::getRealDivideBy0Func(){ if(d_realDivideBy0Func.isNull()){ TypeNode realType = NodeManager::currentNM()->realType(); - d_realDivideBy0Func = skolemFunction("/by0_$$", realType, realType); + d_realDivideBy0Func = skolemFunction("/by0", realType, realType); } return d_realDivideBy0Func; } @@ -237,7 +237,7 @@ Node TheoryArithPrivate::getIntDivideBy0Func(){ if(d_intDivideBy0Func.isNull()){ TypeNode intType = NodeManager::currentNM()->integerType(); - d_intDivideBy0Func = skolemFunction("divby0_$$", intType, intType); + d_intDivideBy0Func = skolemFunction("divby0", intType, intType); } return d_intDivideBy0Func; } @@ -248,7 +248,7 @@ Node TheoryArithPrivate::getIntModulusBy0Func(){ if(d_intModulusBy0Func.isNull()){ TypeNode intType = NodeManager::currentNM()->integerType(); - d_intModulusBy0Func = skolemFunction("modby0_$$", intType, intType); + d_intModulusBy0Func = skolemFunction("modby0", intType, intType); } return d_intModulusBy0Func; } @@ -1498,7 +1498,7 @@ Node TheoryArithPrivate::axiomIteForTotalIntDivision(Node int_div_like){ Polynomial qp = Polynomial::parsePolynomial(q); Node abs_d = (n.isConstant()) ? - d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$"); + d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs"); Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode(); Node leq0 = currNM->mkNode(LEQ, zero, r); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index cd9fd2497..8aad67883 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -845,7 +845,7 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) else { std::hash_map<Node, Node, NodeHashFunction>::iterator it = d_skolemCache.find(n); if (it == d_skolemCache.end()) { - rep = nm->mkSkolem("array_collect_model_var_$$", n.getType(), "base model variable for array collectModelInfo"); + rep = nm->mkSkolem("array_collect_model_var", n.getType(), "base model variable for array collectModelInfo"); d_skolemCache[n] = rep; } else { @@ -963,7 +963,7 @@ void TheoryArrays::check(Effort e) { if(fact[0][0].getType().isArray() && !d_conflict) { NodeManager* nm = NodeManager::currentNM(); TypeNode indexType = fact[0][0].getType()[0]; - TNode k = getSkolem(fact,"array_ext_index_$$", indexType, "an extensional lemma index variable from the theory of arrays", false); + TNode k = getSkolem(fact,"array_ext_index", indexType, "an extensional lemma index variable from the theory of arrays", false); Node ak = nm->mkNode(kind::SELECT, fact[0][0], k); Node bk = nm->mkNode(kind::SELECT, fact[0][1], k); @@ -1574,18 +1574,18 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, } // Solve equation for s: select(s,index) op val --> s = store(s',i',v') /\ index = i' /\ v' op val - Node newVarArr = getSkolem(s, "array_model_arr_var_$$", s.getType(), "a new array variable from the theory of arrays", false); + Node newVarArr = getSkolem(s, "array_model_arr_var", s.getType(), "a new array variable from the theory of arrays", false); Assert(d_infoMap.getModelRep(d_equalityEngine.getRepresentative(newVarArr)).isNull()); Node lookup; bool checkIndex1 = false, checkIndex2 = false, checkIndex3 = false; if (!isLeaf(index)) { - index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays"); + index = getSkolem(index, "array_model_index", index.getType(), "a new index variable from the theory of arrays"); if (!index.getType().isArray()) { checkIndex1 = true; } } lookup = nm->mkNode(kind::SELECT, s, index); - Node newVarVal = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false); + Node newVarVal = getSkolem(lookup, "array_model_var", val.getType(), "a new value variable from the theory of arrays", false); Node newVarVal2; Node index2; @@ -1594,7 +1594,7 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, // Special case: select(s,index) = select(s,j): solution becomes s = store(store(s',j,v'),index,w') /\ v' = w' index2 = val[1]; if (!isLeaf(index2)) { - index2 = getSkolem(val, "array_model_index_$$", index2.getType(), "a new index variable from the theory of arrays"); + index2 = getSkolem(val, "array_model_index", index2.getType(), "a new index variable from the theory of arrays"); if (!index2.getType().isArray()) { checkIndex2 = true; } @@ -1603,7 +1603,7 @@ bool TheoryArrays::setModelVal(TNode node, TNode val, bool invert, bool explain, checkIndex3 = true; } lookup = nm->mkNode(kind::SELECT, s, index2); - newVarVal2 = getSkolem(lookup, "array_model_var_$$", val.getType(), "a new value variable from the theory of arrays", false); + newVarVal2 = getSkolem(lookup, "array_model_var", val.getType(), "a new value variable from the theory of arrays", false); newVarArr = nm->mkNode(kind::STORE, newVarArr, index2, newVarVal2); preRegisterTermInternal(newVarArr); val = newVarVal2; @@ -1927,7 +1927,7 @@ Node TheoryArrays::removeRepLoops(TNode a, TNode rep) // TODO: Change to hasLoop? if (!isLeaf(index)) { changed = true; - index = getSkolem(index, "array_model_index_$$", index.getType(), "a new index variable from the theory of arrays", false); + index = getSkolem(index, "array_model_index", index.getType(), "a new index variable from the theory of arrays", false); if (!d_equalityEngine.hasTerm(index) || !d_equalityEngine.hasTerm(rep[1]) || !d_equalityEngine.areEqual(rep[1], index)) { @@ -1939,7 +1939,7 @@ Node TheoryArrays::removeRepLoops(TNode a, TNode rep) } if (!isLeaf(value)) { changed = true; - value = getSkolem(value, "array_model_var_$$", value.getType(), "a new value variable from the theory of arrays", false); + value = getSkolem(value, "array_model_var", value.getType(), "a new value variable from the theory of arrays", false); if (!d_equalityEngine.hasTerm(value) || !d_equalityEngine.hasTerm(rep[2]) || !d_equalityEngine.areEqual(rep[2], value)) { diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index f35286f05..3c8953e15 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -245,7 +245,7 @@ public: } inline static Node mkGroundTerm(TypeNode type) { Assert(type.getKind() == kind::SORT_TYPE); - return NodeManager::currentNM()->mkSkolem("groundTerm_$$", type, "a ground term created for type " + type.toString()); + return NodeManager::currentNM()->mkSkolem("groundTerm", type, "a ground term created for type " + type.toString()); } };/* class SortProperties */ diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index f35fc2896..95136598c 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -65,7 +65,7 @@ inline Node mkFalse() { inline Node mkVar(unsigned size) { NodeManager* nm = NodeManager::currentNM(); - return nm->mkSkolem("bv_$$", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); + return nm->mkSkolem("bv", nm->mkBitVectorType(size), "is a variable created by the theory of bitvectors"); } diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index dc85d0cd6..389bcca8b 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -266,7 +266,7 @@ public: if( dt.isParametric() ){ tn = TypeNode::fromType( tspec )[i]; } - nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created for inst cons" ); + nc = NodeManager::currentNM()->mkSkolem( "m", tn, "created for inst cons" ); } children.push_back( nc ); } diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index a4af4f26f..35330f81a 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -307,7 +307,7 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed){ return rewritten; }else{ NodeManager* nm = NodeManager::currentNM(); - Node skolem = nm->mkSkolem("compress_$$", nm->booleanType()); + Node skolem = nm->mkSkolem("compress", nm->booleanType()); d_compressed[rewritten] = skolem; d_compressed[original] = skolem; d_compressed[compressed] = skolem; @@ -1175,7 +1175,7 @@ Node ITESimplifier::getSimpVar(TypeNode t) return (*it).second; } else { - Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification"); + Node var = NodeManager::currentNM()->mkSkolem("iteSimp", t, "is a variable resulting from ITE simplification"); d_simpVars[t] = var; return var; } diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index bec8ea350..a294eec5a 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -277,7 +277,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { Node r = d_range[f][v]; if( r.hasBoundVar() ){ //introduce a new bound - Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" ); + Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" ); d_nground_range[f][v] = d_range[f][v]; d_range[f][v] = new_range; r = new_range; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index d5c2b0e9d..098a7819a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -585,7 +585,7 @@ void FirstOrderModelFmc::processInitialize( bool ispre ) { types.push_back(NodeManager::currentNM()->integerType()); } TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() ); - intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" ); + intervalOp = NodeManager::currentNM()->mkSkolem( "interval", typ, "op representing interval" ); } for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ it->second->reset(); @@ -611,7 +611,7 @@ bool FirstOrderModelFmc::isStar(Node n) { Node FirstOrderModelFmc::getStar(TypeNode tn) { std::map<TypeNode, Node >::iterator it = d_type_star.find( tn ); if( it==d_type_star.end() ){ - Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" ); + Node st = NodeManager::currentNM()->mkSkolem( "star", tn, "skolem created for full-model checking" ); d_type_star[tn] = st; st.setAttribute(IsStarAttribute(), true ); return st; diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 126b30b81..0f3e53827 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -591,7 +591,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, types.push_back(f[0][i].getType()); } TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); + Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" ); d_quant_cond[f] = op; } //make sure all types are set @@ -1267,7 +1267,7 @@ Node FullModelChecker::mkArrayCond( Node a ) { if( d_array_term_cond.find(a)==d_array_term_cond.end() ){ if( d_array_cond.find(a.getType())==d_array_cond.end() ){ TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); + Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" ); d_array_cond[a.getType()] = op; } std::vector< Node > cond; diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 435bf7221..72d42cf4b 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -51,7 +51,7 @@ bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite //if value is null, must generate it if( val.isNull() ){ std::stringstream ss; - ss << "mdo_" << it->first << "_$$"; + ss << "mdo_" << it->first << ""; Node op = NodeManager::currentNM()->mkSkolem( ss.str(), it->first.getType(), "op created during macro definitions" ); //will be defined in terms of fresh operator std::vector< Node > children; @@ -273,7 +273,7 @@ void QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod if( d_macro_basis[op].empty() ){ for( size_t a=0; a<m.getNumChildren(); a++ ){ std::stringstream ss; - ss << "mda_" << op << "_$$"; + ss << "mda_" << op << ""; Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); d_macro_basis[op].push_back( v ); } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index a079dbaab..6af42e159 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1154,11 +1154,11 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ //make the new function symbol if( argTypes.empty() ){ - Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" ); + Node s = NodeManager::currentNM()->mkSkolem( "sk", n[0][i].getType(), "created during pre-skolemization" ); subs.push_back( s ); }else{ TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() ); - Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" ); + Node op = NodeManager::currentNM()->mkSkolem( "skop", typ, "op created during pre-skolemization" ); //DOTHIS: set attribute on op, marking that it should not be selected as trigger vector< Node > funcArgs; funcArgs.push_back( op ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e6ee8f53b..3168d21a0 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -413,7 +413,7 @@ Node TermDb::getSkolemizedBody( Node f ){ if( d_skolem_body.find( f )==d_skolem_body.end() ){ std::vector< Node > vars; for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - Node skv = NodeManager::currentNM()->mkSkolem( "skv_$$", f[0][i].getType(), "is a termdb-created skolemized body" ); + Node skv = NodeManager::currentNM()->mkSkolem( "skv", f[0][i].getType(), "is a termdb-created skolemized body" ); d_skolem_constants[ f ].push_back( skv ); vars.push_back( f[0][i] ); //carry information for sort inference @@ -441,7 +441,7 @@ Node TermDb::getFreeVariableForInstConstant( Node n ){ Rational z(0); d_free_vars[tn] = NodeManager::currentNM()->mkConst( z ); }else{ - d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar_$$", tn, "is a free variable created by termdb" ); + d_free_vars[tn] = NodeManager::currentNM()->mkSkolem( "freevar", tn, "is a free variable created by termdb" ); Trace("mkVar") << "FreeVar:: Make variable " << d_free_vars[tn] << " : " << tn << std::endl; } } diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 169688243..2e8eb51b1 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -141,7 +141,7 @@ bool RepSetIterator::initialize(){ TypeNode tn = d_types[i]; if( tn.isSort() ){ if( !d_rep_set->hasType( tn ) ){ - Node var = NodeManager::currentNM()->mkSkolem( "repSet_$$", tn, "is a variable created by the RepSetIterator" ); + Node var = NodeManager::currentNM()->mkSkolem( "repSet", tn, "is a variable created by the RepSetIterator" ); Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( var ); } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f56f509b2..edb245d99 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -760,6 +760,12 @@ bool TheorySetsPrivate::isComplete() { return d_pending.empty() && d_pendingDisequal.empty(); } +Node TheorySetsPrivate::newSkolem(TypeNode t) { + ostringstream oss; + oss << "sde_" << (++d_skolemCounter); + return NodeManager::currentNM()->mkSkolem(oss.str(), t, "", NodeManager::SKOLEM_EXACT_NAME); +} + Node TheorySetsPrivate::getLemma() { Assert(!d_pending.empty() || !d_pendingDisequal.empty()); @@ -780,7 +786,7 @@ Node TheorySetsPrivate::getLemma() { d_pendingEverInserted.insert(n); Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet()); - Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType()); + Node x = newSkolem( n[0].getType().getSetElementType() ); Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]); lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); @@ -806,6 +812,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_pending(u), d_pendingDisequal(u), d_pendingEverInserted(u), + d_skolemCounter(0), d_scrutinize(NULL) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); @@ -1174,8 +1181,8 @@ void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) { (*itb).second->elementsNotInThisSet); /* sets containing this element */ - pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true); - pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false); + // pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true); + // pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false); pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false); pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true); mergeLists( (*ita).second->setsContainingThisElement, diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 7e9d60905..4f2c3c173 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -158,9 +158,11 @@ private: context::CDQueue <TNode> d_pending; context::CDQueue <TNode> d_pendingDisequal; context::CDHashSet <Node, NodeHashFunction> d_pendingEverInserted; + int d_skolemCounter; void addToPending(Node n); bool isComplete(); + Node newSkolem(TypeNode); Node getLemma(); /** model generation and helper function */ diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 0dd43b229..16bb7e694 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -292,7 +292,7 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) { }
}
if(ret == 0) {
- Node sk = NodeManager::currentNM()->mkSkolem( "rsp_$$", NodeManager::currentNM()->stringType(), "Split RegExp" );
+ Node sk = NodeManager::currentNM()->mkSkolem( "rsp", NodeManager::currentNM()->stringType(), "Split RegExp" );
retNode = NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP, sk);
if(!rest.isNull()) {
retNode = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, retNode, rest));
@@ -1030,7 +1030,7 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes emptyflag = true;
break;
} else {
- Node sk = NodeManager::currentNM()->mkSkolem( "rc_$$", s.getType(), "created for regular expression concat" );
+ Node sk = NodeManager::currentNM()->mkSkolem( "rc", s.getType(), "created for regular expression concat" );
Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);
nvec.push_back(lem);
cc.push_back(sk);
@@ -1090,8 +1090,8 @@ void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes } else {
Node se = s.eqNode(d_emptyString);
Node sinr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[0]);
- Node sk1 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );
- Node sk2 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "rs", s.getType(), "created for regular expression star" );
Node s1nz = sk1.eqNode(d_emptyString).negate();
Node s2nz = sk2.eqNode(d_emptyString).negate();
Node s1inr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk1, r[0]);
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d03faa72a..d44f38bc3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -427,8 +427,8 @@ void TheoryStrings::preRegisterTerm(TNode n) { Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[1], d_zero); Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, n[2], d_zero); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" ); d_statistics.d_new_skolems += 2; Node x_eq_123 = n[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, n, sk3 ) ); Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); @@ -1091,9 +1091,9 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, } else { Trace("strings-loop") << "Strings::Loop: Normal Breaking." << std::endl; //right - Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); - Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); - Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop_$$", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); + Node sk_w= NodeManager::currentNM()->mkSkolem( "w_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); + Node sk_y= NodeManager::currentNM()->mkSkolem( "y_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); + Node sk_z= NodeManager::currentNM()->mkSkolem( "z_loop", normal_forms[other_n_index][other_index].getType(), "created for loop detection split" ); d_statistics.d_new_skolems += 3; //t1 * ... * tn = y * z Node conc1 = t_yz.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk_y, sk_z ) ); @@ -1242,7 +1242,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms if( stra.find(fc) == std::string::npos || (stra.find(strb) == std::string::npos && !stra.overlap(strb)) ) { - Node sk = NodeManager::currentNM()->mkSkolem( "sopt_$$", NodeManager::currentNM()->stringType(), "created for string sp" ); + Node sk = NodeManager::currentNM()->mkSkolem( "sopt", NodeManager::currentNM()->stringType(), "created for string sp" ); Node eq = other_str.eqNode( mkConcat(const_str, sk) ); Node ant = mkExplain( antec ); sendLemma(ant, eq, "CST-EPS"); @@ -1254,7 +1254,7 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms NodeManager::currentNM()->mkConst( const_str.getConst<String>().substr(0, 1) ); //split the string Node eq1 = Rewriter::rewrite( other_str.eqNode( d_emptyString ) ); - Node eq2 = mkSplitEq( "c_spt_$$", "created for v/c split", other_str, firstChar, false ); + Node eq2 = mkSplitEq( "c_spt", "created for v/c split", other_str, firstChar, false ); d_pending_req_phase[ eq1 ] = true; conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; @@ -1286,8 +1286,8 @@ bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms } } - Node eq1 = mkSplitEq( "v_spt_l_$$", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true ); - Node eq2 = mkSplitEq( "v_spt_r_$$", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true ); + Node eq1 = mkSplitEq( "v_spt_l", "created for v/v split", normal_forms[i][index_i], normal_forms[j][index_j], true ); + Node eq2 = mkSplitEq( "v_spt_r", "created for v/v split", normal_forms[j][index_j], normal_forms[i][index_i], true ); conc = NodeManager::currentNM()->mkNode( kind::OR, eq1, eq2 ); Node ant = mkExplain( antec, antec_new_lits ); @@ -1588,9 +1588,9 @@ bool TheoryStrings::processDeq( Node ni, Node nj ) { } antec_new_lits.push_back( li.eqNode( lj ).negate() ); std::vector< Node > conc; - Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit_$$", ni.getType(), "created for disequality normalization" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit_$$", ni.getType(), "created for disequality normalization" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit_$$", ni.getType(), "created for disequality normalization" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "x_dsplit", ni.getType(), "created for disequality normalization" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "y_dsplit", ni.getType(), "created for disequality normalization" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "z_dsplit", ni.getType(), "created for disequality normalization" ); d_statistics.d_new_skolems += 3; //Node nemp = sk1.eqNode(d_emptyString).negate(); //conc.push_back(nemp); @@ -1910,7 +1910,7 @@ bool TheoryStrings::checkSimple() { Node sk; //if( d_length_inst.find(n)==d_length_inst.end() ) { //Node nr = d_equalityEngine.getRepresentative( n ); - sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" ); + sk = NodeManager::currentNM()->mkSkolem( "lsym", n.getType(), "created for length" ); d_statistics.d_new_skolems += 1; d_length_intro_vars.insert( sk ); Node eq = sk.eqNode(n); @@ -2497,10 +2497,10 @@ bool TheoryStrings::checkMemberships() { }else{ Trace("strings-regexp-debug") << "Case 2\n"; std::vector< Node > conc_c; - Node s11 = NodeManager::currentNM()->mkSkolem( "s11_$$", NodeManager::currentNM()->stringType(), "created for re" ); - Node s12 = NodeManager::currentNM()->mkSkolem( "s12_$$", NodeManager::currentNM()->stringType(), "created for re" ); - Node s21 = NodeManager::currentNM()->mkSkolem( "s21_$$", NodeManager::currentNM()->stringType(), "created for re" ); - Node s22 = NodeManager::currentNM()->mkSkolem( "s22_$$", NodeManager::currentNM()->stringType(), "created for re" ); + Node s11 = NodeManager::currentNM()->mkSkolem( "s11", NodeManager::currentNM()->stringType(), "created for re" ); + Node s12 = NodeManager::currentNM()->mkSkolem( "s12", NodeManager::currentNM()->stringType(), "created for re" ); + Node s21 = NodeManager::currentNM()->mkSkolem( "s21", NodeManager::currentNM()->stringType(), "created for re" ); + Node s22 = NodeManager::currentNM()->mkSkolem( "s22", NodeManager::currentNM()->stringType(), "created for re" ); conc = p1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s11, s12)); conc_c.push_back(conc); conc = p2.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s21, s22)); @@ -2666,8 +2666,8 @@ bool TheoryStrings::checkPosContains() { Node s = atom[1]; if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) { if(d_pos_ctn_cached.find(atom) == d_pos_ctn_cached.end()) { - Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1", s.getType(), "created for contain" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2", s.getType(), "created for contain" ); d_statistics.d_new_skolems += 2; Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) ); sendLemma( atom, eq, "POS-INC" ); diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 1b040f71c..85ab73691 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -184,8 +184,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node t1geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[1], d_zero); Node t2geq0 = NodeManager::currentNM()->mkNode(kind::GEQ, t[2], d_zero); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3_$$", NodeManager::currentNM()->stringType(), "created for charat/substr" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "ss1", NodeManager::currentNM()->stringType(), "created for charat/substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "ss3", NodeManager::currentNM()->stringType(), "created for charat/substr" ); Node x_eq_123 = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, t, sk3 ) ); Node len_sk1_eq_i = t[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); Node lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, @@ -196,11 +196,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { d_cache[t] = t; } else if( t.getKind() == kind::STRING_STRIDOF ) { if(options::stringExp()) { - Node sk1 = NodeManager::currentNM()->mkSkolem( "io1_$$", t[0].getType(), "created for indexof" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "io2_$$", t[0].getType(), "created for indexof" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "io3_$$", t[0].getType(), "created for indexof" ); - Node sk4 = NodeManager::currentNM()->mkSkolem( "io4_$$", t[0].getType(), "created for indexof" ); - Node skk = NodeManager::currentNM()->mkSkolem( "iok_$$", t[2].getType(), "created for indexof" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "io1", t[0].getType(), "created for indexof" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "io2", t[0].getType(), "created for indexof" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "io3", t[0].getType(), "created for indexof" ); + Node sk4 = NodeManager::currentNM()->mkSkolem( "io4", t[0].getType(), "created for indexof" ); + Node skk = NodeManager::currentNM()->mkSkolem( "iok", t[2].getType(), "created for indexof" ); Node eq = t[0].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3, sk4 ) ); new_nodes.push_back( eq ); Node negone = NodeManager::currentNM()->mkConst( ::CVC4::Rational(-1) ); @@ -274,11 +274,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { std::vector< TypeNode > argTypes; argTypes.push_back(NodeManager::currentNM()->integerType()); - Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", + Node ufP = NodeManager::currentNM()->mkSkolem("ufP", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->integerType()), "uf type conv P"); - Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", + Node ufM = NodeManager::currentNM()->mkSkolem("ufM", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->integerType()), "uf type conv M"); @@ -368,11 +368,11 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node ten = NodeManager::currentNM()->mkConst( ::CVC4::Rational(10) ); std::vector< TypeNode > argTypes; argTypes.push_back(NodeManager::currentNM()->integerType()); - Node ufP = NodeManager::currentNM()->mkSkolem("ufP_$$", + Node ufP = NodeManager::currentNM()->mkSkolem("ufP", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->integerType()), "uf type conv P"); - Node ufM = NodeManager::currentNM()->mkSkolem("ufM_$$", + Node ufM = NodeManager::currentNM()->mkSkolem("ufM", NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->integerType()), "uf type conv M"); @@ -404,9 +404,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { //cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1); //cc2 std::vector< Node > vec_n; - Node z1 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType()); - Node z2 = NodeManager::currentNM()->mkSkolem("z2_$$", NodeManager::currentNM()->stringType()); - Node z3 = NodeManager::currentNM()->mkSkolem("z3_$$", NodeManager::currentNM()->stringType()); + Node z1 = NodeManager::currentNM()->mkSkolem("z1", NodeManager::currentNM()->stringType()); + Node z2 = NodeManager::currentNM()->mkSkolem("z2", NodeManager::currentNM()->stringType()); + Node z3 = NodeManager::currentNM()->mkSkolem("z3", NodeManager::currentNM()->stringType()); Node g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) ); vec_n.push_back(g); g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) ); @@ -499,9 +499,9 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node x = t[0]; Node y = t[1]; Node z = t[2]; - Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1_$$", t[0].getType(), "created for replace" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2_$$", t[0].getType(), "created for replace" ); - Node skw = NodeManager::currentNM()->mkSkolem( "rpw_$$", t[0].getType(), "created for replace" ); + Node sk1 = NodeManager::currentNM()->mkSkolem( "rp1", t[0].getType(), "created for replace" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "rp2", t[0].getType(), "created for replace" ); + Node skw = NodeManager::currentNM()->mkSkolem( "rpw", t[0].getType(), "created for replace" ); Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y ); Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) ); Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index d171c739d..e4778e86c 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -307,7 +307,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); TypeNode t = (*it).getType(check); if (!t.isRegExp()) { throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); @@ -323,7 +322,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); TypeNode t = (*it).getType(check); if (!t.isRegExp()) { throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); @@ -339,7 +337,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); TypeNode t = (*it).getType(check); if (!t.isRegExp()) { throw TypeCheckingExceptionPrivate(n, "expecting regexp terms"); @@ -355,7 +352,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); char ch[2]; for(int i=0; i<2; ++i) { @@ -422,7 +418,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); TypeNode t = (*it).getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms"); @@ -441,7 +436,6 @@ public: throw (TypeCheckingExceptionPrivate, AssertionException) { if( check ) { TNode::iterator it = n.begin(); - TNode::iterator it_end = n.end(); TypeNode t = (*it).getType(check); if (!t.isString()) { throw TypeCheckingExceptionPrivate(n, "expecting string terms"); diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 115788639..7509c7f4f 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -92,7 +92,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - Node n = NodeManager::currentNM()->mkSkolem("unconstrained_$$", t, "a new var introduced because of unconstrained variable " + var.toString()); + Node n = NodeManager::currentNM()->mkSkolem("unconstrained", t, "a new var introduced because of unconstrained variable " + var.toString()); return n; } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 1cfd5cd5c..bf3f1a873 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -94,7 +94,9 @@ libutil_la_SOURCES = \ sort_inference.h \ sort_inference.cpp \ regexp.h \ - regexp.cpp + regexp.cpp \ + didyoumean.h \ + didyoumean.cpp libstatistics_la_SOURCES = \ statistics_registry.h \ diff --git a/src/util/didyoumean.cpp b/src/util/didyoumean.cpp new file mode 100644 index 000000000..d64435ce7 --- /dev/null +++ b/src/util/didyoumean.cpp @@ -0,0 +1,145 @@ +/********************* */ +/*! \file didyoumean.cpp + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief did-you-mean style suggestions + ** + ** ``What do you mean? I don't understand.'' An attempt to be more + ** helpful than that. Similar to one in git. + ** + ** There are no dependencies on CVC4, intentionally. + **/ + +#include "didyoumean.h" +#include <iostream> +#include <sstream> +#include <boost/foreach.hpp> +#include <boost/algorithm/string/predicate.hpp> +using namespace std; + +vector<string> DidYouMean::getMatch(string input) { + /** Magic numbers */ + const int similarityThreshold = 7; + const unsigned numMatchesThreshold = 10; + + set< pair<int, string> > scores; + vector<string> ret; + BOOST_FOREACH(string s, d_words ) { + if( s == input ) { + // if input matches AS-IS just return that + ret.push_back(s); + return ret; + } + int score; + if(boost::starts_with(s, input)) { + score = 0; + } else { + score = editDistance(input, s) + 1; + } + scores.insert( make_pair(score, s) ); + } + int min_score = scores.begin()->first; + for(typeof(scores.begin()) i = scores.begin(); + i != scores.end(); ++i) { + + // add if score is overall not too big, and also not much close to + // the score of the best suggestion + if(i->first < similarityThreshold && i->first <= min_score + 1) { + ret.push_back(i->second); +#ifdef DIDYOUMEAN_DEBUG + cout << i->second << ": " << i->first << std::endl; +#endif + } + } + if(ret.size() > numMatchesThreshold ) ret.resize(numMatchesThreshold);; + return ret; +} + + +int DidYouMean::editDistance(const std::string& a, const std::string& b) +{ + // input string: a + // desired string: b + + const int swapCost = 0; + const int substituteCost = 2; + const int addCost = 1; + const int deleteCost = 3; + const int switchCaseCost = 0; + + int len1 = a.size(); + int len2 = b.size(); + + int C[3][len2+1]; // cost + + for(int j = 0; j <= len2; ++j) { + C[0][j] = j * addCost; + } + + for(int i = 1; i <= len1; ++i) { + + int cur = i%3; + int prv = (i+2)%3; + int pr2 = (i+1)%3; + + C[cur][0] = i * deleteCost; + + for(int j = 1; j <= len2; ++j) { + + C[cur][j] = 100000000; // INF + + if(a[i-1] == b[j-1]) { + // match + C[cur][j] = std::min(C[cur][j], C[prv][j-1]); + } else if(tolower(a[i-1]) == tolower(b[j-1])){ + // switch case + C[cur][j] = std::min(C[cur][j], C[prv][j-1] + switchCaseCost); + } else { + // substitute + C[cur][j] = std::min(C[cur][j], C[prv][j-1] + substituteCost); + } + + // swap + if(i >= 2 && j >= 2 && a[i-1] == b[j-2] && a[i-2] == b[j-1]) { + C[cur][j] = std::min(C[cur][j], C[pr2][j-2] + swapCost); + } + + // add + C[cur][j] = std::min(C[cur][j], C[cur][j-1] + addCost); + + // delete + C[cur][j] = std::min(C[cur][j], C[prv][j] + deleteCost); + +#ifdef DIDYOUMEAN_DEBUG1 + std::cout << "C[" << cur << "][" << 0 << "] = " << C[cur][0] << std::endl; +#endif + } + + } + return C[len1%3][len2]; +} + +string DidYouMean::getMatchAsString(string input, int prefixNewLines, int suffixNewLines) { + vector<string> matches = getMatch(input); + ostringstream oss; + if(matches.size() > 0) { + while(prefixNewLines --> 0) { oss << endl; } + if(matches.size() == 1) { + oss << "Did you mean this?"; + } else { + oss << "Did you mean any of these?"; + } + for(unsigned i = 0; i < matches.size(); ++i) { + oss << "\n " << matches[i]; + } + while(suffixNewLines --> 0) { oss << endl; } + } + return oss.str(); +} diff --git a/src/util/didyoumean.h b/src/util/didyoumean.h new file mode 100644 index 000000000..2907fcece --- /dev/null +++ b/src/util/didyoumean.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file didyoumean.h + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief did-you-mean style suggestions. + ** + ** ``What do you mean? I don't understand.'' An attempt to be more + ** helpful than that. Similar to one in git. + ** + ** There are no dependencies on CVC4, intentionally. + **/ + +#pragma once + +#include <vector> +#include <set> +#include <string> + +class DidYouMean { + typedef std::set<std::string> Words; + Words d_words; + +public: + DidYouMean() {} + ~DidYouMean() {} + + DidYouMean(Words words) : d_words(words) {} + + void addWord(std::string word) { + d_words.insert(word); + } + + std::vector<std::string> getMatch(std::string input); + + /** + * This is provided to make it easier to ensure consistency of + * output. Returned string is empty if there are no matches. + */ + std::string getMatchAsString(std::string input, int prefixNewLines = 2, int suffixNewLines = 0); +private: + int editDistance(const std::string& a, const std::string& b); +}; diff --git a/src/util/didyoumean_test.cpp b/src/util/didyoumean_test.cpp new file mode 100644 index 000000000..5aa7cc105 --- /dev/null +++ b/src/util/didyoumean_test.cpp @@ -0,0 +1,748 @@ +// Compile: g++ didyoumean_test.cpp didyoumean.cpp +// For debug compile with -DDIDYOUMEAN_DEBUG or -DDIDYOUMEAN_DEBUG1 or both + +#include "didyoumean.h" +#include <iostream> +#include <boost/foreach.hpp> +using namespace std; + +set<string> getDebugTags(); +set<string> getOptionStrings(); + +int main() +{ + string a, b; + + cin >> a; + cout << "Matches with debug tags:" << endl; + vector<string> ret = DidYouMean(getDebugTags()).getMatch(a); + BOOST_FOREACH(string s, ret) cout << s << endl; + cout << "Matches with option strings:" << endl; + ret = DidYouMean(getOptionStrings()).getMatch(a); + BOOST_FOREACH(string s, ret) cout << s << endl; +} + +set<string> getDebugTags() +{ + set<string> a; + a.insert("CDInsertHashMap"); + a.insert("CDTrailHashMap"); + a.insert("TrailHashMap"); + a.insert("approx"); + a.insert("approx::"); + a.insert("approx::branch"); + a.insert("approx::checkCutOnPad"); + a.insert("approx::constraint"); + a.insert("approx::gmi"); + a.insert("approx::gmiCut"); + a.insert("approx::guessIsConstructable"); + a.insert("approx::lemmas"); + a.insert("approx::mir"); + a.insert("approx::mirCut"); + a.insert("approx::nodelog"); + a.insert("approx::replayAssert"); + a.insert("approx::replayLogRec"); + a.insert("approx::soi"); + a.insert("approx::solveMIP"); + a.insert("approx::sumConstraints"); + a.insert("approx::vars"); + a.insert("arith"); + a.insert("arith::addSharedTerm"); + a.insert("arith::approx::cuts"); + a.insert("arith::arithvar"); + a.insert("arith::asVectors"); + a.insert("arith::bt"); + a.insert("arith::collectModelInfo"); + a.insert("arith::conflict"); + a.insert("arith::congruenceManager"); + a.insert("arith::congruences"); + a.insert("arith::consistency"); + a.insert("arith::consistency::comitonconflict"); + a.insert("arith::consistency::final"); + a.insert("arith::consistency::initial"); + a.insert("arith::constraint"); + a.insert("arith::dio"); + a.insert("arith::dio::ex"); + a.insert("arith::dio::max"); + a.insert("arith::div"); + a.insert("arith::dual"); + a.insert("arith::ems"); + a.insert("arith::eq"); + a.insert("arith::error::mem"); + a.insert("arith::explain"); + a.insert("arith::explainNonbasics"); + a.insert("arith::findModel"); + a.insert("arith::focus"); + a.insert("arith::hasIntegerModel"); + a.insert("arith::importSolution"); + a.insert("arith::ite"); + a.insert("arith::ite::red"); + a.insert("arith::learned"); + a.insert("arith::lemma"); + a.insert("arith::nf"); + a.insert("arith::oldprop"); + a.insert("arith::pivot"); + a.insert("arith::preprocess"); + a.insert("arith::preregister"); + a.insert("arith::presolve"); + a.insert("arith::print_assertions"); + a.insert("arith::print_model"); + a.insert("arith::prop"); + a.insert("arith::resolveOutPropagated"); + a.insert("arith::restart"); + a.insert("arith::rewriter"); + a.insert("arith::selectPrimalUpdate"); + a.insert("arith::simplex:row"); + a.insert("arith::solveInteger"); + a.insert("arith::static"); + a.insert("arith::subsumption"); + a.insert("arith::tracking"); + a.insert("arith::tracking::mid"); + a.insert("arith::tracking::post"); + a.insert("arith::tracking::pre"); + a.insert("arith::unate"); + a.insert("arith::unate::conf"); + a.insert("arith::update"); + a.insert("arith::update::select"); + a.insert("arith::value"); + a.insert("array-pf"); + a.insert("array-types"); + a.insert("arrays"); + a.insert("arrays-model-based"); + a.insert("arrays::propagate"); + a.insert("arrays::sharing"); + a.insert("attrgc"); + a.insert("basicsAtBounds"); + a.insert("bitvector"); + a.insert("bitvector-bb"); + a.insert("bitvector-bitblast"); + a.insert("bitvector-expandDefinition"); + a.insert("bitvector-model"); + a.insert("bitvector-preregister"); + a.insert("bitvector-rewrite"); + a.insert("bitvector::bitblaster"); + a.insert("bitvector::core"); + a.insert("bitvector::explain"); + a.insert("bitvector::propagate"); + a.insert("bitvector::sharing"); + a.insert("bool-flatten"); + a.insert("bool-ite"); + a.insert("boolean-terms"); + a.insert("bt"); + a.insert("builder"); + a.insert("bv-bitblast"); + a.insert("bv-core"); + a.insert("bv-core-model"); + a.insert("bv-inequality"); + a.insert("bv-inequality-explain"); + a.insert("bv-inequality-internal"); + a.insert("bv-rewrite"); + a.insert("bv-slicer"); + a.insert("bv-slicer-eq"); + a.insert("bv-slicer-uf"); + a.insert("bv-subtheory-inequality"); + a.insert("bv-to-bool"); + a.insert("bva"); + a.insert("bvminisat"); + a.insert("bvminisat::explain"); + a.insert("bvminisat::search"); + a.insert("cbqi"); + a.insert("cbqi-debug"); + a.insert("cbqi-prop-as-dec"); + a.insert("cd_set_collection"); + a.insert("cdlist"); + a.insert("cdlist:cmm"); + a.insert("cdqueue"); + a.insert("check-inst"); + a.insert("check-model::rep-checking"); + a.insert("circuit-prop"); + a.insert("cnf"); + a.insert("constructInfeasiblityFunction"); + a.insert("context"); + a.insert("current"); + a.insert("datatypes"); + a.insert("datatypes-cycle-check"); + a.insert("datatypes-cycles"); + a.insert("datatypes-cycles-find"); + a.insert("datatypes-debug"); + a.insert("datatypes-explain"); + a.insert("datatypes-gt"); + a.insert("datatypes-inst"); + a.insert("datatypes-labels"); + a.insert("datatypes-output"); + a.insert("datatypes-parametric"); + a.insert("datatypes-prereg"); + a.insert("datatypes-split"); + a.insert("decision"); + a.insert("decision::jh"); + a.insert("determineArithVar"); + a.insert("diamonds"); + a.insert("dio::push"); + a.insert("dt"); + a.insert("dt-enum"); + a.insert("dt-warn"); + a.insert("dt::propagate"); + a.insert("dualLike"); + a.insert("effortlevel"); + a.insert("ensureLiteral"); + a.insert("eq"); + a.insert("equality"); + a.insert("equality::backtrack"); + a.insert("equality::disequality"); + a.insert("equality::evaluation"); + a.insert("equality::graph"); + a.insert("equality::internal"); + a.insert("equality::trigger"); + a.insert("equalsConstant"); + a.insert("error"); + a.insert("estimateWithCFE"); + a.insert("expand"); + a.insert("export"); + a.insert("flipdec"); + a.insert("fmc-entry-trie"); + a.insert("fmc-interval-model-debug"); + a.insert("fmf-card-debug"); + a.insert("fmf-eval-debug"); + a.insert("fmf-eval-debug2"); + a.insert("fmf-exit"); + a.insert("fmf-index-order"); + a.insert("fmf-model-complete"); + a.insert("fmf-model-cons"); + a.insert("fmf-model-cons-debug"); + a.insert("fmf-model-eval"); + a.insert("fmf-model-prefs"); + a.insert("fmf-model-req"); + a.insert("focusDownToJust"); + a.insert("focusDownToLastHalf"); + a.insert("foo"); + a.insert("gaussianElimConstructTableRow"); + a.insert("gc"); + a.insert("gc:leaks"); + a.insert("getBestImpliedBound"); + a.insert("getCeiling"); + a.insert("getNewDomainValue"); + a.insert("getPropagatedLiterals"); + a.insert("getType"); + a.insert("glpk::loadVB"); + a.insert("guessCoefficientsConstructTableRow"); + a.insert("guessIsConstructable"); + a.insert("handleBorders"); + a.insert("includeBoundUpdate"); + a.insert("inst"); + a.insert("inst-engine"); + a.insert("inst-engine-ctrl"); + a.insert("inst-engine-debug"); + a.insert("inst-engine-phase-req"); + a.insert("inst-engine-stuck"); + a.insert("inst-fmf-ei"); + a.insert("inst-match-gen"); + a.insert("inst-trigger"); + a.insert("integers"); + a.insert("interactive"); + a.insert("intersectConstantIte"); + a.insert("isConst"); + a.insert("ite"); + a.insert("ite::atom"); + a.insert("ite::constantIteEqualsConstant"); + a.insert("ite::print-success"); + a.insert("ite::simpite"); + a.insert("lemma-ites"); + a.insert("lemmaInputChannel"); + a.insert("literal-matching"); + a.insert("logPivot"); + a.insert("matrix"); + a.insert("minisat"); + a.insert("minisat::lemmas"); + a.insert("minisat::pop"); + a.insert("minisat::remove-clause"); + a.insert("minisat::search"); + a.insert("miplib"); + a.insert("model"); + a.insert("model-getvalue"); + a.insert("nf::tmp"); + a.insert("nm"); + a.insert("normal-form"); + a.insert("options"); + a.insert("paranoid:check_tableau"); + a.insert("parser"); + a.insert("parser-extra"); + a.insert("parser-idt"); + a.insert("parser-param"); + a.insert("partial_model"); + a.insert("pb"); + a.insert("pickle"); + a.insert("pickler"); + a.insert("pipe"); + a.insert("portfolio::outputmode"); + a.insert("prec"); + a.insert("preemptGetopt"); + a.insert("proof:sat"); + a.insert("proof:sat:detailed"); + a.insert("prop"); + a.insert("prop-explain"); + a.insert("prop-value"); + a.insert("prop::lemmas"); + a.insert("propagateAsDecision"); + a.insert("properConflict"); + a.insert("qcf-ccbe"); + a.insert("qcf-check-inst"); + a.insert("qcf-eval"); + a.insert("qcf-match"); + a.insert("qcf-match-debug"); + a.insert("qcf-nground"); + a.insert("qint-check-debug2"); + a.insert("qint-debug"); + a.insert("qint-error"); + a.insert("qint-model-debug"); + a.insert("qint-model-debug2"); + a.insert("qint-var-order-debug2"); + a.insert("quant-arith"); + a.insert("quant-arith-debug"); + a.insert("quant-arith-simplex"); + a.insert("quant-datatypes"); + a.insert("quant-datatypes-debug"); + a.insert("quant-req-phase"); + a.insert("quant-uf-strategy"); + a.insert("quantifiers"); + a.insert("quantifiers-assert"); + a.insert("quantifiers-check"); + a.insert("quantifiers-dec"); + a.insert("quantifiers-engine"); + a.insert("quantifiers-flip"); + a.insert("quantifiers-other"); + a.insert("quantifiers-prereg"); + a.insert("quantifiers-presolve"); + a.insert("quantifiers-relevance"); + a.insert("quantifiers-sat"); + a.insert("quantifiers-substitute-debug"); + a.insert("quantifiers::collectModelInfo"); + a.insert("queueConditions"); + a.insert("rationalToCfe"); + a.insert("recentlyViolated"); + a.insert("register"); + a.insert("register::internal"); + a.insert("relevant-trigger"); + a.insert("removeFixed"); + a.insert("rl"); + a.insert("sat::minisat"); + a.insert("selectFocusImproving"); + a.insert("set_collection"); + a.insert("sets"); + a.insert("sets-assert"); + a.insert("sets-checkmodel-ignore"); + a.insert("sets-eq"); + a.insert("sets-learn"); + a.insert("sets-lemma"); + a.insert("sets-model"); + a.insert("sets-model-details"); + a.insert("sets-parent"); + a.insert("sets-pending"); + a.insert("sets-prop"); + a.insert("sets-prop-details"); + a.insert("sets-scrutinize"); + a.insert("sets-terminfo"); + a.insert("shared"); + a.insert("shared-terms-database"); + a.insert("shared-terms-database::assert"); + a.insert("sharing"); + a.insert("simple-trigger"); + a.insert("simplify"); + a.insert("smart-multi-trigger"); + a.insert("smt"); + a.insert("soi::findModel"); + a.insert("soi::selectPrimalUpdate"); + a.insert("solveRealRelaxation"); + a.insert("sort"); + a.insert("speculativeUpdate"); + a.insert("strings"); + a.insert("strings-explain"); + a.insert("strings-explain-debug"); + a.insert("strings-prereg"); + a.insert("strings-propagate"); + a.insert("substitution"); + a.insert("substitution::internal"); + a.insert("tableau"); + a.insert("te"); + a.insert("term-db-cong"); + a.insert("theory"); + a.insert("theory::assertions"); + a.insert("theory::atoms"); + a.insert("theory::bv::rewrite"); + a.insert("theory::conflict"); + a.insert("theory::explain"); + a.insert("theory::idl"); + a.insert("theory::idl::model"); + a.insert("theory::internal"); + a.insert("theory::propagate"); + a.insert("trans-closure"); + a.insert("treat-unknown-error"); + a.insert("tuprec"); + a.insert("typecheck-idt"); + a.insert("typecheck-q"); + a.insert("typecheck-r"); + a.insert("uf"); + a.insert("uf-ss"); + a.insert("uf-ss-check-region"); + a.insert("uf-ss-cliques"); + a.insert("uf-ss-debug"); + a.insert("uf-ss-disequal"); + a.insert("uf-ss-na"); + a.insert("uf-ss-region"); + a.insert("uf-ss-region-debug"); + a.insert("uf-ss-register"); + a.insert("uf-ss-sat"); + a.insert("uf::propagate"); + a.insert("uf::sharing"); + a.insert("ufgc"); + a.insert("ufsymm"); + a.insert("ufsymm:clauses"); + a.insert("ufsymm:eq"); + a.insert("ufsymm:match"); + a.insert("ufsymm:norm"); + a.insert("ufsymm:p"); + a.insert("update"); + a.insert("updateAndSignal"); + a.insert("weak"); + a.insert("whytheoryenginewhy"); + return a; +} + +set<string> getOptionStrings() +{ + const char* cmdlineOptions[] = { + "lang", + "output-lang", + "language", + "output-language", + "verbose", + "quiet", + "stats", + "no-stats", + "statistics", + "no-statistics", + "stats-every-query", + "no-stats-every-query", + "statistics-every-query", + "no-statistics-every-query", + "parse-only", + "no-parse-only", + "preprocess-only", + "no-preprocess-only", + "trace", + "debug", + "print-success", + "no-print-success", + "smtlib-strict", + "default-expr-depth", + "default-dag-thresh", + "print-expr-types", + "eager-type-checking", + "lazy-type-checking", + "no-type-checking", + "biased-ites", + "no-biased-ites", + "boolean-term-conversion-mode", + "theoryof-mode", + "use-theory", + "bitblast-eager", + "no-bitblast-eager", + "bitblast-share-lemmas", + "no-bitblast-share-lemmas", + "bitblast-eager-fullcheck", + "no-bitblast-eager-fullcheck", + "bv-inequality-solver", + "no-bv-inequality-solver", + "bv-core-solver", + "no-bv-core-solver", + "bv-to-bool", + "no-bv-to-bool", + "bv-propagate", + "no-bv-propagate", + "bv-eq", + "no-bv-eq", + "dt-rewrite-error-sel", + "no-dt-rewrite-error-sel", + "dt-force-assignment", + "unate-lemmas", + "arith-prop", + "heuristic-pivots", + "standard-effort-variable-order-pivots", + "error-selection-rule", + "simplex-check-period", + "pivot-threshold", + "prop-row-length", + "disable-dio-solver", + "enable-arith-rewrite-equalities", + "disable-arith-rewrite-equalities", + "enable-miplib-trick", + "disable-miplib-trick", + "miplib-trick-subs", + "cut-all-bounded", + "no-cut-all-bounded", + "maxCutsInContext", + "revert-arith-models-on-unsat", + "no-revert-arith-models-on-unsat", + "fc-penalties", + "no-fc-penalties", + "use-fcsimplex", + "no-use-fcsimplex", + "use-soi", + "no-use-soi", + "restrict-pivots", + "no-restrict-pivots", + "collect-pivot-stats", + "no-collect-pivot-stats", + "use-approx", + "no-use-approx", + "approx-branch-depth", + "dio-decomps", + "no-dio-decomps", + "new-prop", + "no-new-prop", + "arith-prop-clauses", + "soi-qe", + "no-soi-qe", + "rewrite-divk", + "no-rewrite-divk", + "se-solve-int", + "no-se-solve-int", + "lemmas-on-replay-failure", + "no-lemmas-on-replay-failure", + "dio-turns", + "rr-turns", + "dio-repeat", + "no-dio-repeat", + "replay-early-close-depth", + "replay-failure-penalty", + "replay-num-err-penalty", + "replay-reject-cut", + "replay-lemma-reject-cut", + "replay-soi-major-threshold", + "replay-soi-major-threshold-pen", + "replay-soi-minor-threshold", + "replay-soi-minor-threshold-pen", + "symmetry-breaker", + "no-symmetry-breaker", + "condense-function-values", + "no-condense-function-values", + "disable-uf-ss-regions", + "uf-ss-eager-split", + "no-uf-ss-eager-split", + "uf-ss-totality", + "no-uf-ss-totality", + "uf-ss-totality-limited", + "uf-ss-totality-sym-break", + "no-uf-ss-totality-sym-break", + "uf-ss-abort-card", + "uf-ss-explained-cliques", + "no-uf-ss-explained-cliques", + "uf-ss-simple-cliques", + "no-uf-ss-simple-cliques", + "uf-ss-deq-prop", + "no-uf-ss-deq-prop", + "disable-uf-ss-min-model", + "uf-ss-clique-splits", + "no-uf-ss-clique-splits", + "uf-ss-sym-break", + "no-uf-ss-sym-break", + "uf-ss-fair", + "no-uf-ss-fair", + "arrays-optimize-linear", + "no-arrays-optimize-linear", + "arrays-lazy-rintro1", + "no-arrays-lazy-rintro1", + "arrays-model-based", + "no-arrays-model-based", + "arrays-eager-index", + "no-arrays-eager-index", + "arrays-eager-lemmas", + "no-arrays-eager-lemmas", + "disable-miniscope-quant", + "disable-miniscope-quant-fv", + "disable-prenex-quant", + "disable-var-elim-quant", + "disable-ite-lift-quant", + "cnf-quant", + "no-cnf-quant", + "clause-split", + "no-clause-split", + "pre-skolem-quant", + "no-pre-skolem-quant", + "ag-miniscope-quant", + "no-ag-miniscope-quant", + "macros-quant", + "no-macros-quant", + "fo-prop-quant", + "no-fo-prop-quant", + "disable-smart-triggers", + "relevant-triggers", + "no-relevant-triggers", + "relational-triggers", + "no-relational-triggers", + "register-quant-body-terms", + "no-register-quant-body-terms", + "inst-when", + "eager-inst-quant", + "no-eager-inst-quant", + "full-saturate-quant", + "no-full-saturate-quant", + "literal-matching", + "enable-cbqi", + "no-enable-cbqi", + "cbqi-recurse", + "no-cbqi-recurse", + "user-pat", + "flip-decision", + "disable-quant-internal-reps", + "finite-model-find", + "no-finite-model-find", + "mbqi", + "mbqi-one-inst-per-round", + "no-mbqi-one-inst-per-round", + "mbqi-one-quant-per-round", + "no-mbqi-one-quant-per-round", + "fmf-inst-engine", + "no-fmf-inst-engine", + "disable-fmf-inst-gen", + "fmf-inst-gen-one-quant-per-round", + "no-fmf-inst-gen-one-quant-per-round", + "fmf-fresh-dc", + "no-fmf-fresh-dc", + "disable-fmf-fmc-simple", + "fmf-bound-int", + "no-fmf-bound-int", + "axiom-inst", + "quant-cf", + "no-quant-cf", + "quant-cf-mode", + "quant-cf-when", + "rewrite-rules", + "no-rewrite-rules", + "rr-one-inst-per-round", + "no-rr-one-inst-per-round", + "strings-exp", + "no-strings-exp", + "strings-lb", + "strings-fmf", + "no-strings-fmf", + "strings-eit", + "no-strings-eit", + "strings-alphabet-card", + "show-sat-solvers", + "random-freq", + "random-seed", + "restart-int-base", + "restart-int-inc", + "refine-conflicts", + "no-refine-conflicts", + "minisat-elimination", + "no-minisat-elimination", + "minisat-dump-dimacs", + "no-minisat-dump-dimacs", + "model-format", + "dump", + "dump-to", + "force-logic", + "simplification", + "no-simplification", + "static-learning", + "no-static-learning", + "produce-models", + "no-produce-models", + "check-models", + "no-check-models", + "dump-models", + "no-dump-models", + "proof", + "no-proof", + "check-proofs", + "no-check-proofs", + "dump-proofs", + "no-dump-proofs", + "produce-unsat-cores", + "no-produce-unsat-cores", + "produce-assignments", + "no-produce-assignments", + "interactive", + "no-interactive", + "ite-simp", + "no-ite-simp", + "on-repeat-ite-simp", + "no-on-repeat-ite-simp", + "simp-with-care", + "no-simp-with-care", + "simp-ite-compress", + "no-simp-ite-compress", + "unconstrained-simp", + "no-unconstrained-simp", + "repeat-simp", + "no-repeat-simp", + "simp-ite-hunt-zombies", + "sort-inference", + "no-sort-inference", + "incremental", + "no-incremental", + "abstract-values", + "no-abstract-values", + "model-u-dt-enum", + "no-model-u-dt-enum", + "tlimit", + "tlimit-per", + "rlimit", + "rlimit-per", + "rewrite-apply-to-const", + "no-rewrite-apply-to-const", + "replay", + "replay-log", + "decision", + "decision-threshold", + "decision-use-weight", + "no-decision-use-weight", + "decision-random-weight", + "decision-weight-internal", + "version", + "license", + "help", + "show-config", + "show-debug-tags", + "show-trace-tags", + "early-exit", + "no-early-exit", + "threads", + "threadN", + "filter-lemma-length", + "fallback-sequential", + "no-fallback-sequential", + "incremental-parallel", + "no-incremental-parallel", + "no-interactive-prompt", + "continued-execution", + "immediate-exit", + "segv-spin", + "no-segv-spin", + "segv-nospin", + "wait-to-join", + "no-wait-to-join", + "strict-parsing", + "no-strict-parsing", + "mmap", + "no-mmap", + "no-checking", + "no-filesystem-access", + "no-include-file", + "enable-idl-rewrite-equalities", + "disable-idl-rewrite-equalities", + "sets-propagate", + "no-sets-propagate", + "sets-eager-lemmas", + "no-sets-eager-lemmas", + NULL, + };/* cmdlineOptions */ + int i = 0; + set<string> ret; + while(cmdlineOptions[i] != NULL) { + ret.insert(cmdlineOptions[i]); + i++; + } + return ret; +} diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index 1b29f9ef8..f1dce413c 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -93,7 +93,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { Node skolem; // Make the skolem to represent the ITE - skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal"); + skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); // The new assertion Node newAssertion = diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index 682e1e1e7..ce12b59f1 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -504,7 +504,7 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ return NodeManager::currentNM()->mkBoundVar( ss.str(), tn ); }else{ std::stringstream ss; - ss << "i_$$_" << old; + ss << "i_" << old; return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" ); } } @@ -576,7 +576,7 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ } if( opChanged ){ std::stringstream ss; - ss << "io_$$_" << op; + ss << "io_" << op; TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); }else{ @@ -622,7 +622,7 @@ Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { std::vector< TypeNode > tns; tns.push_back( tn1 ); TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 ); - Node f = NodeManager::currentNM()->mkSkolem( "inj_$$", typ, "injection for monotonicity constraint" ); + Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" ); Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 ); Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 ); diff --git a/test/regress/regress0/arrayinuf_error.smt2 b/test/regress/regress0/arrayinuf_error.smt2 index d029b2b6a..dd5fd58a7 100644 --- a/test/regress/regress0/arrayinuf_error.smt2 +++ b/test/regress/regress0/arrayinuf_error.smt2 @@ -1,4 +1,8 @@ -; EXPECT-ERROR: (error "Parse Error: arrayinuf_error.smt2:3.21: Symbol 'Array' not declared as a type") +; EXPECT-ERROR: (error "Parse Error: arrayinuf_error.smt2:7.21: Symbol 'Array' not declared as a type +; EXPECT-ERROR: +; EXPECT-ERROR: (declare-fun a (Array Bool Bool)) +; EXPECT-ERROR: ^ +; EXPECT-ERROR: ") (set-logic QF_UF) (declare-fun a (Array Bool Bool)) ; EXIT: 1 diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc index dd3db0fdd..de4d8e1a7 100644 --- a/test/regress/regress0/error.cvc +++ b/test/regress/regress0/error.cvc @@ -1,4 +1,8 @@ % EXPECT-ERROR: CVC4 Error: -% EXPECT-ERROR: Parse Error: error.cvc:3.8: Symbol 'BOOL' not declared as a type +% EXPECT-ERROR: Parse Error: error.cvc:7.8: Symbol 'BOOL' not declared as a type +% EXPECT-ERROR: +% EXPECT-ERROR: p : BOOL; +% EXPECT-ERROR: ^ +% EXPECT-ERROR: p : BOOL; % EXIT: 1 diff --git a/test/regress/run_regression b/test/regress/run_regression index bf4dcc6ef..f0ffd765d 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -185,6 +185,7 @@ gettemp expoutfile cvc4_expect_stdout.$$.XXXXXXXXXX gettemp experrfile cvc4_expect_stderr.$$.XXXXXXXXXX gettemp outfile cvc4_stdout.$$.XXXXXXXXXX gettemp errfile cvc4_stderr.$$.XXXXXXXXXX +gettemp errfilefix cvc4_stderr.$$.XXXXXXXXXX gettemp exitstatusfile cvc4_exitstatus.$$.XXXXXXXXXX if [ -z "$expected_output" ]; then @@ -247,9 +248,20 @@ else ) > "$outfile" 2> "$errfile" ) fi +# we have to actual error file same treatment as other files. differences in +# versions of echo/bash were causing failure on some platforms and not on others +actual_error=$(cat $errfile) +if [ -z "$actual_error" ]; then + # in case expected stderr output is empty, make sure we don't differ + # by a newline, which we would if we echo "" >"$experrfile" + touch "$errfilefix" +else + echo "$actual_error" >"$errfilefix" +fi + diffs=`diff -u --strip-trailing-cr "$expoutfile" "$outfile"` diffexit=$? -diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfile"` +diffserr=`diff -u --strip-trailing-cr "$experrfile" "$errfilefix"` diffexiterr=$? exit_status=`cat "$exitstatusfile"` |