Implement :named and let abbreviation modes in ExprSMTLIBPrinter

* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET)
* Remove the now defunct ExprSMTLIBLetPrinter
* Improve performance of ExprSMTLIBPrinter::scan() by keeping
  track of visited Expr to avoid visiting them again
* Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()

2 files changed, 123 insertions, 259 deletions

diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp
deleted file mode 100644
index d4243452..00000000
--- a/lib/Expr/ExprSMTLIBLetPrinter.cpp
+++ /dev/null
@@ -1,232 +0,0 @@
-//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*-
-//C++ -*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "llvm/Support/raw_ostream.h"
-#include "llvm/Support/CommandLine.h"
-#include "klee/util/ExprSMTLIBLetPrinter.h"
-
-namespace ExprSMTLIBOptions {
-llvm::cl::opt<bool>
-useLetExpressions("smtlib-use-let-expressions",
-                  llvm::cl::desc("Enables generated SMT-LIBv2 files to use "
-                                 "(let) expressions (default=on)"),
-                  llvm::cl::init(true));
-}
-
-namespace klee {
-const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
-
-ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter()
-    : bindings(), firstEO(), twoOrMoreEO(), disablePrintedAbbreviations(false) {
-}
-
-void ExprSMTLIBLetPrinter::generateOutput() {
-  if (p == NULL || query == NULL || o == NULL) {
-    llvm::errs() << "Can't print SMTLIBv2. Output or query bad!\n";
-    return;
-  }
-
-  generateBindings();
-
-  if (isHumanReadable())
-    printNotice();
-  printOptions();
-  printSetLogic();
-  printArrayDeclarations();
-  printLetExpression();
-  printAction();
-  printExit();
-}
-
-void ExprSMTLIBLetPrinter::scan(const ref<Expr> &e) {
-  if (isa<ConstantExpr>(e))
-    return; // we don't need to scan simple constants
-
-  if (firstEO.insert(e).second) {
-    // We've not seen this expression before
-
-    if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
-
-      // Attempt to insert array and if array wasn't present before do more
-      // things
-      if (usedArrays.insert(re->updates.root).second) {
-
-        // check if the array is constant
-        if (re->updates.root->isConstantArray())
-          haveConstantArray = true;
-
-        // scan the update list
-        scanUpdates(re->updates.head);
-      }
-    }
-
-    // recurse into the children
-    Expr *ep = e.get();
-    for (unsigned int i = 0; i < ep->getNumKids(); i++)
-      scan(ep->getKid(i));
-  } else {
-    /* We must of seen the expression before. Add it to
-     * the set of twoOrMoreOccurances. We don't need to
-     * check if the insertion fails.
-     */
-    twoOrMoreEO.insert(e);
-  }
-}
-
-void ExprSMTLIBLetPrinter::generateBindings() {
-  // Assign a number to each binding that will be used
-  unsigned int counter = 0;
-  for (std::set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
-       i != twoOrMoreEO.end(); ++i) {
-    bindings.insert(std::make_pair(*i, counter));
-    ++counter;
-  }
-}
-
-void ExprSMTLIBLetPrinter::printExpression(
-    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
-  std::map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e);
-
-  if (disablePrintedAbbreviations || i == bindings.end()) {
-    /*There is no abbreviation for this expression so print it normally.
-     * Do this by using the parent method.
-     */
-    ExprSMTLIBPrinter::printExpression(e, expectedSort);
-  } else {
-    // Use binding name e.g. "?B1"
-
-    /* Handle the corner case where the expectedSort
-     * doesn't match the sort of the abbreviation. Not really very efficient
-     * (calls bindings.find() twice),
-     * we'll cast and call ourself again but with the correct expectedSort.
-     */
-    if (getSort(e) != expectedSort) {
-      printCastToSort(e, expectedSort);
-      return;
-    }
-
-    // No casting is needed in this depth of recursion, just print the
-    // abbreviation
-    *p << BINDING_PREFIX << i->second;
-  }
-}
-
-void ExprSMTLIBLetPrinter::reset() {
-  // Let parent clean up first
-  ExprSMTLIBPrinter::reset();
-
-  firstEO.clear();
-  twoOrMoreEO.clear();
-  bindings.clear();
-}
-
-void ExprSMTLIBLetPrinter::printLetExpression() {
-  *p << "(assert";
-  p->pushIndent();
-  printSeperator();
-
-  if (bindings.size() != 0) {
-    // Only print let expression if we have bindings to use.
-    *p << "(let";
-    p->pushIndent();
-    printSeperator();
-    *p << "( ";
-    p->pushIndent();
-
-    // Print each binding
-    for (std::map<const ref<Expr>, unsigned int>::const_iterator i =
-             bindings.begin();
-         i != bindings.end(); ++i) {
-      printSeperator();
-      *p << "(" << BINDING_PREFIX << i->second << " ";
-      p->pushIndent();
-
-      // Disable abbreviations so none are used here.
-      disablePrintedAbbreviations = true;
-
-      // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
-      printExpression(i->first, getSort(i->first));
-
-      p->popIndent();
-      printSeperator();
-      *p << ")";
-    }
-
-    p->popIndent();
-    printSeperator();
-    *p << ")";
-    printSeperator();
-
-    // Re-enable printing abbreviations.
-    disablePrintedAbbreviations = false;
-  }
-
-  // print out Expressions with abbreviations.
-  unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query
-  unsigned int itemsLeft = numberOfItems;
-  std::vector<ref<Expr> >::const_iterator constraint =
-      query->constraints.begin();
-
-  /* Produce nested (and () () statements. If the constraint set
-   * is empty then we will only print the "queryAssert".
-   */
-  for (; itemsLeft != 0; --itemsLeft) {
-    if (itemsLeft >= 2) {
-      *p << "(and";
-      p->pushIndent();
-      printSeperator();
-      printExpression(*constraint,
-                      SORT_BOOL); // We must and together bool expressions
-      printSeperator();
-      ++constraint;
-      continue;
-    } else {
-      // must have 1 item left (i.e. the "queryAssert")
-      if (isHumanReadable()) {
-        *p << "; query";
-        p->breakLineI();
-      }
-      printExpression(queryAssert,
-                      SORT_BOOL); // The query must be a bool expression
-    }
-  }
-
-  /* Produce closing brackets for nested "and statements".
-   * Number of "nested ands" = numberOfItems -1
-   */
-  itemsLeft = numberOfItems - 1;
-  for (; itemsLeft != 0; --itemsLeft) {
-    p->popIndent();
-    printSeperator();
-    *p << ")";
-  }
-
-  if (bindings.size() != 0) {
-    // end let expression
-    p->popIndent();
-    printSeperator();
-    *p << ")";
-    printSeperator();
-  }
-
-  // end assert
-  p->popIndent();
-  printSeperator();
-  *p << ")";
-  p->breakLineI();
-}
-
-ExprSMTLIBPrinter *createSMTLIBPrinter() {
-  if (ExprSMTLIBOptions::useLetExpressions)
-    return new ExprSMTLIBLetPrinter();
-  else
-    return new ExprSMTLIBPrinter();
-}
-}
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index bbb82d0d..fb7e270e 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -31,6 +31,19 @@ llvm::cl::opt<bool> humanReadableSMTLIB(
     llvm::cl::desc(
         "Enables generated SMT-LIBv2 files to be human readable (default=off)"),
     llvm::cl::init(false));
+
+llvm::cl::opt<klee::ExprSMTLIBPrinter::AbbreviationMode> abbreviationMode(
+    "smtlib-abbreviation-mode",
+    llvm::cl::desc(
+        "Choose abbreviation mode to use in SMT-LIBv2 files (default=let)"),
+    llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NONE, "none",
+                                "Do not abbreviate"),
+                     clEnumValN(klee::ExprSMTLIBPrinter::ABBR_LET, "let",
+                                "Abbreviate with let"),
+                     clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NAMED, "named",
+                                "Abbreviate with :named annotations"),
+                     clEnumValEnd),
+    llvm::cl::init(klee::ExprSMTLIBPrinter::ABBR_LET));
 }
 
 namespace klee {
@@ -41,6 +54,7 @@ ExprSMTLIBPrinter::ExprSMTLIBPrinter()
       humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB),
       smtlibBoolOptions(), arraysToCallGetValueOn(NULL) {
   setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode);
+  setAbbreviationMode(ExprSMTLIBOptions::abbreviationMode);
 }
 
 ExprSMTLIBPrinter::~ExprSMTLIBPrinter() {
@@ -60,10 +74,11 @@ void ExprSMTLIBPrinter::setQuery(const Query &q) {
   query = &q;
   reset(); // clear the data structures
   scanAll();
-  negateQueryExpression();
 }
 
 void ExprSMTLIBPrinter::reset() {
+  bindings.clear();
+  seenExprs.clear();
   usedArrays.clear();
   haveConstantArray = false;
 
@@ -154,6 +169,41 @@ void ExprSMTLIBPrinter::printExpression(
     return;
   }
 
+  switch (abbrMode) {
+  case ABBR_NONE:
+    break;
+
+  case ABBR_LET: {
+    BindingMap::iterator i = bindings.find(e);
+    if (i != bindings.end()) {
+      *p << "?B" << i->second;
+      return;
+    }
+    break;
+  }
+
+  case ABBR_NAMED: {
+    BindingMap::iterator i = bindings.find(e);
+    if (i != bindings.end()) {
+      if (i->second > 0) {
+        *p << "(! ";
+        printFullExpression(e, expectedSort);
+        *p << " :named ?B" << i->second << ")";
+        i->second = -i->second;
+      } else {
+        *p << "?B" << -i->second;
+      }
+      return;
+    }
+    break;
+  }
+  }
+
+  printFullExpression(e, expectedSort);
+}
+
+void ExprSMTLIBPrinter::printFullExpression(
+    const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
   switch (e->getKind()) {
   case Expr::Constant:
     printConstant(cast<ConstantExpr>(e));
@@ -431,7 +481,7 @@ void ExprSMTLIBPrinter::generateOutput() {
   printSetLogic();
   printArrayDeclarations();
   printConstraints();
-  printQuery();
+  printQueryExpr();
   printAction();
   printExit();
 }
@@ -576,24 +626,32 @@ void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
   if (isa<ConstantExpr>(e))
     return; // we don't need to scan simple constants
 
-  if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
+  if (seenExprs.insert(e).second) {
+    // We've not seen this expression before
+
+    if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
 
-    // Attempt to insert array and if array wasn't present before do more things
-    if (usedArrays.insert(re->updates.root).second) {
+      // Attempt to insert array and if array wasn't present before do more things
+      if (usedArrays.insert(re->updates.root).second) {
 
-      // check if the array is constant
-      if (re->updates.root->isConstantArray())
-        haveConstantArray = true;
+        // check if the array is constant
+        if (re->updates.root->isConstantArray())
+          haveConstantArray = true;
 
-      // scan the update list
-      scanUpdates(re->updates.head);
+        // scan the update list
+        scanUpdates(re->updates.head);
+      }
     }
-  }
 
-  // recurse into the children
-  Expr *ep = e.get();
-  for (unsigned int i = 0; i < ep->getNumKids(); i++)
-    scan(ep->getKid(i));
+    // recurse into the children
+    Expr *ep = e.get();
+    for (unsigned int i = 0; i < ep->getNumKids(); i++)
+      scan(ep->getKid(i));
+  } else {
+    // Add the expression to the binding map. The semantics of std::map::insert
+    // are such that it will not be inserted twice.
+    bindings.insert(std::make_pair(e, bindings.size()+1));
+  }
 }
 
 void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) {
@@ -637,18 +695,52 @@ void ExprSMTLIBPrinter::printOptions() {
   }
 }
 
-void ExprSMTLIBPrinter::printQuery() {
-  if (humanReadable) {
-    *p << "; Query from solver turned into an assert";
-    p->breakLineI();
-  }
-
+void ExprSMTLIBPrinter::printAssert(const ref<Expr> &e) {
   p->pushIndent();
   *p << "(assert";
   p->pushIndent();
   printSeperator();
 
-  printExpression(queryAssert, SORT_BOOL);
+  if (abbrMode == ABBR_LET && bindings.size() != 0) {
+    // Only print let expression if we have bindings to use.
+    *p << "(let";
+    p->pushIndent();
+    printSeperator();
+    *p << "( ";
+    p->pushIndent();
+
+    // Disable abbreviations so none are used here.
+    abbrMode = ABBR_NONE;
+
+    // Print each binding
+    for (BindingMap::const_iterator i = bindings.begin(); i != bindings.end();
+         ++i) {
+      printSeperator();
+      *p << "(?B" << i->second << " ";
+      p->pushIndent();
+
+      // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
+      printExpression(i->first, getSort(i->first));
+
+      p->popIndent();
+      printSeperator();
+      *p << ")";
+    }
+
+    // Re-enable printing abbreviations.
+    abbrMode = ABBR_LET;
+
+    p->popIndent();
+    printSeperator();
+    *p << ")";
+    printSeperator();
+
+    printExpression(e, SORT_BOOL);
+
+    *p << ")";
+  } else {
+    printExpression(e, SORT_BOOL);
+  }
 
   p->popIndent();
   printSeperator();
@@ -657,6 +749,15 @@ void ExprSMTLIBPrinter::printQuery() {
   p->breakLineI();
 }
 
+void ExprSMTLIBPrinter::printQueryExpr() {
+  if (humanReadable) {
+    *p << "; Query from solver turned into an assert";
+    p->breakLineI();
+  }
+  ref<Expr> queryAssert = Expr::createIsZero(query->expr);
+  printAssert(queryAssert);
+}
+
 ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr> &e) {
   switch (e->getKind()) {
   case Expr::NotOptimized:
@@ -831,11 +932,6 @@ void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(
   *p << ")";
 }
 
-void ExprSMTLIBPrinter::negateQueryExpression() {
-  // Negating the query
-  queryAssert = Expr::createIsZero(query->expr);
-}
-
 bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option,
                                             SMTLIBboolValues value) {
   std::pair<std::map<SMTLIBboolOptions, bool>::iterator, bool> thePair;