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, 54 insertions, 104 deletions

diff --git a/include/klee/util/ExprSMTLIBLetPrinter.h b/include/klee/util/ExprSMTLIBLetPrinter.h
deleted file mode 100644
index dd97e0d5..00000000
--- a/include/klee/util/ExprSMTLIBLetPrinter.h
+++ /dev/null
@@ -1,73 +0,0 @@
-//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++
-//-*-===//
-//
-//                     The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "ExprSMTLIBPrinter.h"
-#ifndef EXPRSMTLETPRINTER_H_
-#define EXPRSMTLETPRINTER_H_
-
-namespace klee {
-/// This printer behaves like ExprSMTLIBPrinter except that it will abbreviate
-/// expressions
-/// using the (let) SMT-LIBv2 command. Expression trees that appear two or more
-/// times in the Query
-/// passed to setQuery() will be abbreviated.
-///
-/// This class should be used just like ExprSMTLIBPrinter.
-class ExprSMTLIBLetPrinter : public ExprSMTLIBPrinter {
-public:
-  ExprSMTLIBLetPrinter();
-  virtual ~ExprSMTLIBLetPrinter() {}
-  virtual void generateOutput();
-
-protected:
-  virtual void scan(const ref<Expr> &e);
-  virtual void reset();
-  virtual void generateBindings();
-  void printExpression(const ref<Expr> &e,
-                       ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
-  void printLetExpression();
-
-private:
-  /// Let expression binding number map.
-  std::map<const ref<Expr>, unsigned int> bindings;
-
-  /* These are effectively expression counters.
-   * firstEO - first Occurrence of expression contains
-   *           all expressions that occur once. It is
-   *           only used to help us fill twoOrMoreOE
-   *
-   * twoOrMoreEO - Contains occur all expressions that
-   *               that occur two or more times. These
-   *               are the expressions that will be
-   *               abbreviated by using (let () ()) expressions.
-   *
-   *
-   *
-   */
-  std::set<ref<Expr> > firstEO, twoOrMoreEO;
-
-  /// This is the prefix string used for all abbreviations in (let) expressions.
-  static const char BINDING_PREFIX[];
-
-  /* This is needed during un-abbreviated printing.
-   * Because we have overloaded printExpression()
-   * the parent will call it and will abbreviate
-   * when we don't want it to. This bool allows us
-   * to switch it on/off easily.
-   */
-  bool disablePrintedAbbreviations;
-};
-
-/// Create a SMT-LIBv2 printer based on command line options
-/// The caller is responsible for deleting the printer
-ExprSMTLIBPrinter *createSMTLIBPrinter();
-}
-
-#endif /* EXPRSMTLETPRINTER_H_ */
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h
index 8b072242..ff024e11 100644
--- a/include/klee/util/ExprSMTLIBPrinter.h
+++ b/include/klee/util/ExprSMTLIBPrinter.h
@@ -30,8 +30,7 @@ namespace klee {
 /// set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is
 /// set to QF_ABV.
 ///
-/// This printer does not abbreviate expressions. The printer
-/// ExprSMTLIBLetPrinter does though.
+/// This printer abbreviates expressions according to its abbreviation mode.
 ///
 /// It is intended to be used as follows
 /// -# Create instance of this class
@@ -109,6 +108,14 @@ public:
     DECIMAL ///< Display bit vector constants in Decimal e.g. (_ bv45 8)
   };
 
+  /// How to abbreviate repeatedly mentioned expressions. Some solvers do not
+  /// understand all of them, hence the flexibility.
+  enum AbbreviationMode {
+    ABBR_NONE, ///< Do not abbreviate.
+    ABBR_LET,  ///< Abbreviate with let.
+    ABBR_NAMED ///< Abbreviate with :named annotations.
+  };
+
   /// Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV
   enum SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL };
 
@@ -119,6 +126,8 @@ public:
 
   ConstantDisplayMode getConstantDisplayMode() { return cdm; }
 
+  void setAbbreviationMode(AbbreviationMode am) { abbrMode = am; }
+
   /// Create a new printer that will print a query in the SMTLIBv2 language.
   ExprSMTLIBPrinter();
 
@@ -131,7 +140,7 @@ public:
   /// the SMTLIBv2 (get-value ()) command).
   void setQuery(const Query &q);
 
-  virtual ~ExprSMTLIBPrinter();
+  ~ExprSMTLIBPrinter();
 
   /// Print the query to the llvm::raw_ostream
   /// setOutput() and setQuery() must be called before calling this.
@@ -150,7 +159,7 @@ public:
   /// is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet()
   /// then the setSMTLIBboolOption()
   /// call will be ineffective.
-  virtual void generateOutput();
+  void generateOutput();
 
   /// Set which SMTLIBv2 logic to use.
   /// This only affects what logic is used in the (set-logic <logic>) command.
@@ -204,6 +213,16 @@ protected:
   /// Contains the arrays found during scans
   std::set<const Array *> usedArrays;
 
+  /// Set of expressions seen during scan.
+  std::set<ref<Expr> > seenExprs;
+
+  typedef std::map<const ref<Expr>, int> BindingMap;
+
+  /// Let expression binding number map. Under the :named abbreviation mode,
+  /// negative binding numbers indicate that the abbreviation has already been
+  /// emitted, so it may be used.
+  BindingMap bindings;
+
   /// Output stream to write to
   llvm::raw_ostream *o;
 
@@ -217,36 +236,36 @@ protected:
   void printCastToSort(const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT sort);
 
   // Resets various internal objects for a new query
-  virtual void reset();
+  void reset();
 
   // Scan all constraints and the query
-  virtual void scanAll();
+  void scanAll();
 
   // Print an initial SMTLIBv2 comment before anything else is printed
-  virtual void printNotice();
+  void printNotice();
 
   // Print SMTLIBv2 options e.g. (set-option :option-name <value>) command
-  virtual void printOptions();
+  void printOptions();
 
   // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV)
-  virtual void printSetLogic();
+  void printSetLogic();
 
   // Print SMTLIBv2 assertions for constant arrays
-  virtual void printArrayDeclarations();
+  void printArrayDeclarations();
 
   // Print SMTLIBv2 for all constraints in the query
-  virtual void printConstraints();
+  void printConstraints();
 
   // Print SMTLIBv2 assert statement for the negated query expression
-  virtual void printQuery();
+  void printQueryExpr();
 
   /// Print the SMTLIBv2 command to check satisfiability and also optionally
   /// request for values
   /// \sa setArrayValuesToGet()
-  virtual void printAction();
+  void printAction();
 
   /// Print the SMTLIBv2 command to exit
-  virtual void printExit();
+  void printExit();
 
   /// Print a Constant in the format specified by the current "Constant Display
   /// Mode"
@@ -256,13 +275,13 @@ protected:
   /// \param e is the expression to print
   /// \param expectedSort is the sort we want. If "e" is not of the right type a
   /// cast will be performed.
-  virtual void printExpression(const ref<Expr> &e,
-                               ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
+  /// \param abbrMode the abbreviation mode to use for this expression
+  void printExpression(const ref<Expr> &e, SMTLIB_SORT expectedSort);
 
   /// Scan Expression recursively for Arrays in expressions. Found arrays are
   /// added to
   /// the usedArrays vector.
-  virtual void scan(const ref<Expr> &e);
+  void scan(const ref<Expr> &e);
 
   /* Rules of recursion for "Special Expression handlers" and
    *printSortArgsExpr()
@@ -280,15 +299,15 @@ protected:
    */
 
   // Special Expression handlers
-  virtual void printReadExpr(const ref<ReadExpr> &e);
-  virtual void printExtractExpr(const ref<ExtractExpr> &e);
-  virtual void printCastExpr(const ref<CastExpr> &e);
-  virtual void printNotEqualExpr(const ref<NeExpr> &e);
-  virtual void printSelectExpr(const ref<SelectExpr> &e,
+  void printReadExpr(const ref<ReadExpr> &e);
+  void printExtractExpr(const ref<ExtractExpr> &e);
+  void printCastExpr(const ref<CastExpr> &e);
+  void printNotEqualExpr(const ref<NeExpr> &e);
+  void printSelectExpr(const ref<SelectExpr> &e,
                                ExprSMTLIBPrinter::SMTLIB_SORT s);
 
   // For the set of operators that take sort "s" arguments
-  virtual void printSortArgsExpr(const ref<Expr> &e,
+  void printSortArgsExpr(const ref<Expr> &e,
                                  ExprSMTLIBPrinter::SMTLIB_SORT s);
 
   /// For the set of operators that come in two sorts (e.g. (and () ()) (bvand
@@ -296,21 +315,21 @@ protected:
   /// These are and,xor,or,not
   /// \param e the Expression to print
   /// \param s the sort of the expression we want
-  virtual void printLogicalOrBitVectorExpr(const ref<Expr> &e,
+  void printLogicalOrBitVectorExpr(const ref<Expr> &e,
                                            ExprSMTLIBPrinter::SMTLIB_SORT s);
 
   /// Recursively prints updatesNodes
-  virtual void printUpdatesAndArray(const UpdateNode *un, const Array *root);
+  void printUpdatesAndArray(const UpdateNode *un, const Array *root);
 
   /// This method does the translation between Expr classes and SMTLIBv2
   /// keywords
   /// \return A C-string of the SMTLIBv2 keyword
-  virtual const char *getSMTLIBKeyword(const ref<Expr> &e);
+  const char *getSMTLIBKeyword(const ref<Expr> &e);
 
-  virtual void printSeperator();
+  void printSeperator();
 
   /// Helper function for scan() that scans the expressions of an update node
-  virtual void scanUpdates(const UpdateNode *un);
+  void scanUpdates(const UpdateNode *un);
 
   /// Helper printer class
   PrintContext *p;
@@ -330,18 +349,22 @@ private:
   // Map of enabled SMTLIB Options
   std::map<SMTLIBboolOptions, bool> smtlibBoolOptions;
 
-  /// This sets queryAssert to be the boolean negation of the original Query
-  void negateQueryExpression();
-
   // Print a SMTLIBv2 option as a C-string
   const char *
   getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option);
 
+  /// Print expression without top-level abbreviations
+  void printFullExpression(const ref<Expr> &e, SMTLIB_SORT expectedSort);
+
+  /// Print an assert statement for the given expr.
+  void printAssert(const ref<Expr> &e);
+
   // Pointer to a vector of Arrays. These will be used for the (get-value () )
   // call.
   const std::vector<const Array *> *arraysToCallGetValueOn;
 
   ConstantDisplayMode cdm;
+  AbbreviationMode abbrMode;
 };
 }