1 files changed, 0 insertions, 107 deletions
diff --git a/stp/AST/ASTUtil.h b/stp/AST/ASTUtil.h
deleted file mode 100644
index c90ee0ce..00000000
--- a/stp/AST/ASTUtil.h
+++ /dev/null
@@ -1,107 +0,0 @@
-/********************************************************************
- * AUTHORS: Vijay Ganesh, David L. Dill
- *
- * BEGIN DATE: November, 2005
- *
- * LICENSE: Please view LICENSE file in the home dir of this Program
- ********************************************************************/
-// -*- c++ -*-
-
-#ifndef ASTUTIL_H
-#define ASTUTIL_H
-
-#include <cstring>
-#include <iostream>
-#include <vector>
-#ifdef EXT_HASH_MAP
-#include <ext/hash_set>
-#include <ext/hash_map>
-#else
-#include <hash_set>
-#include <hash_map>
-#endif
-
-using namespace std; 
-namespace BEEV {
-#ifdef EXT_HASH_MAP
-  using namespace __gnu_cxx;
-#endif
-  //some global variables that are set through commandline options. it
-  //is best that these variables remain global. Default values set
-  //here
-  //
-  //collect statistics on certain functions
-  extern bool stats;
-  //print DAG nodes
-  extern bool print_nodes;
-  //tentative global var to allow for variable activity optimization
-  //in the SAT solver. deprecated.
-  extern bool variable_activity_optimize;
-  //run STP in optimized mode
-  extern bool optimize;
-  //do sat refinement, i.e. underconstraint the problem, and feed to
-  //SAT. if this works, great. else, add a set of suitable constraints
-  //to re-constraint the problem correctly, and call SAT again, until
-  //all constraints have been added.
-  extern bool arrayread_refinement;
-  //switch to control write refinements
-  extern bool arraywrite_refinement;
-  //check the counterexample against the original input to STP
-  extern bool check_counterexample;
-  //construct the counterexample in terms of original variable based
-  //on the counterexample returned by SAT solver
-  extern bool construct_counterexample;
-  extern bool print_counterexample;
-  //if this option is true then print the way dawson wants using a
-  //different printer. do not use this printer.
-  extern bool print_arrayval_declaredorder;
-  //flag to decide whether to print "valid/invalid" or not
-  extern bool print_output;
-  //do linear search in the array values of an input array. experimental
-  extern bool linear_search;
-  //print the variable order chosen by the sat solver while it is
-  //solving.
-  extern bool print_sat_varorder; 
-  //turn on word level bitvector solver
-  extern bool wordlevel_solve;
-  //XOR flattening optimizations.
-  extern bool xor_flatten;
-  //this flag indicates that the BVSolver() succeeded
-  extern bool toplevel_solved;
-  //the smtlib parser has been turned on
-  extern bool smtlib_parser_enable;
-  //print the input back
-  extern bool print_STPinput_back;
-
-  extern void (*vc_error_hdlr)(const char* err_msg);
-  /*Spacer class is basically just an int, but the new class allows
-    overloading of << with a special definition that prints the int as
-    that many spaces. */
-  class Spacer {
-  public:
-    int _spaces;
-    Spacer(int spaces) { _spaces = spaces; }
-    friend ostream& operator<<(ostream& os, const Spacer &ind);
-  };
-
-  inline Spacer spaces(int width) {
-    Spacer sp(width);
-    return sp;
-  }
-
-  struct eqstr {
-    bool operator()(const char* s1, const char* s2) const {
-      return strcmp(s1, s2) == 0;
-    }
-  };
-  
-  typedef hash_map<const char*,int, 
-		   hash<const char *>,eqstr> function_counters;
-  void CountersAndStats(const char * functionname);
-
-  //global function which accepts an integer and looks up the
-  //corresponding ASTNode and prints a char* of that ASTNode
-  void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, 
-					   int decision, int polarity=0);
-} // end namespace.
-#endif