Dagification of output expressions.

By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables.
This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N
times, it is dagified; a setting of 0 turns off dagification entirely.

If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior
with --default-expr-dag=0 and let me know of the problem.

2 files changed, 23 insertions, 3 deletions

diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h
index 5e04f820d..3714fcccc 100644
--- a/src/util/node_visitor.h
+++ b/src/util/node_visitor.h
@@ -32,7 +32,7 @@ template<typename Visitor>
 class NodeVisitor {
 
   /** For re-entry checking */
-  static CVC4_THREADLOCAL(bool) d_inRun;
+  static CVC4_THREADLOCAL(bool) s_inRun;
 
   class GuardReentry {
     bool& d_guard;
@@ -69,7 +69,7 @@ public:
    */
   static typename Visitor::return_type run(Visitor& visitor, TNode node) {
 
-    GuardReentry guard(bool(d_inRun));
+    GuardReentry guard(bool(s_inRun));
 
     // Notify of a start
     visitor.start(node);
@@ -111,7 +111,7 @@ public:
 };
 
 template <typename Visitor>
-CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::d_inRun = false;
+CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false;
 
 }
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 78eea71ad..a6bd9d09a 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -194,6 +194,8 @@ Additional CVC4 options:\n\
    --show-trace-tags      show all avalable tags for tracing\n\
    --show-sat-solvers     show all available SAT solvers\n\
    --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
+   --default-dag-thresh=N dagify common subexprs appearing > N times\n\
+                          (1 == default, 0 == don't dagify)\n\
    --print-expr-types     print types with variables when printing exprs\n\
    --lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
    --simplification=MODE  choose simplification mode, see --simplification=help\n\
@@ -454,6 +456,7 @@ enum OptionValue {
   SHOW_CONFIG,
   STRICT_PARSING,
   DEFAULT_EXPR_DEPTH,
+  DEFAULT_DAG_THRESH,
   PRINT_EXPR_TYPES,
   UF_THEORY,
   LAZY_DEFINITION_EXPANSION,
@@ -557,6 +560,7 @@ static struct option cmdlineOptions[] = {
   { "mmap"       , no_argument      , NULL, USE_MMAP    },
   { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
   { "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
+  { "default-dag-thresh", required_argument, NULL, DEFAULT_DAG_THRESH },
   { "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
   { "uf"         , required_argument, NULL, UF_THEORY   },
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
@@ -832,6 +836,22 @@ throw(OptionException) {
       }
       break;
 
+    case DEFAULT_DAG_THRESH:
+      {
+        int dag = atoi(optarg);
+        if(dag < 0) {
+          throw OptionException("--default-dag-thresh requires a nonnegative argument.");
+        }
+        Debug.getStream() << Expr::dag(size_t(dag));
+        Trace.getStream() << Expr::dag(size_t(dag));
+        Notice.getStream() << Expr::dag(size_t(dag));
+        Chat.getStream() << Expr::dag(size_t(dag));
+        Message.getStream() << Expr::dag(size_t(dag));
+        Warning.getStream() << Expr::dag(size_t(dag));
+        Dump.getStream() << Expr::dag(size_t(dag));
+      }
+      break;
+
     case PRINT_EXPR_TYPES:
       Debug.getStream() << Expr::printtypes(true);
       Trace.getStream() << Expr::printtypes(true);