Refactor. Automatically layout code.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1518 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h
index f1b80d8b2a5e202dcfd11219cfdff769260b2e9b..3b2f3af9bf9f0c5970f0b96656e12968c7e40a1f 100644 (file)
--- a/src/cpp_interface/cpp_interface.h
+++ b/src/cpp_interface/cpp_interface.h
@@ -1,4 +1,3 @@
-
 #ifndef CPP_INTERFACE_H_
 #define CPP_INTERFACE_H_
 
@@ -12,243 +11,263 @@
 
 namespace BEEV
 {
-using BEEV::STPMgr;
-
+  using BEEV::STPMgr;
 
 // There's no BVTypeCheck() function. Use a typechecking node factory instead.
 
-class Cpp_interface
-{
-       STPMgr& bm;
-       //boost::object_pool<ASTNode> node_pool;
-       bool alreadyWarned;
-       bool print_success;
-public:
-       LETMgr letMgr;
-       NodeFactory* nf;
-
-       Cpp_interface(STPMgr &bm_, NodeFactory* factory)
-       : bm(bm_),
-         nf(factory),
-         letMgr(bm.ASTUndefined)
-       {
-               assert(nf != NULL);
-               alreadyWarned = false;
-               cache.push_back(Entry(SOLVER_UNDECIDED));
-               symbols.push_back(ASTVec());
-               print_success=false;
-       }
-
-       const ASTVec GetAsserts(void)
-       {
-               return bm.GetAsserts();
-       }
+  class Cpp_interface
+  {
+    STPMgr& bm;
+    //boost::object_pool<ASTNode> node_pool;
+    bool alreadyWarned;
+    bool print_success;
+  public:
+    LETMgr letMgr;
+    NodeFactory* nf;
+
+    Cpp_interface(STPMgr &bm_, NodeFactory* factory) :
+        bm(bm_), nf(factory), letMgr(bm.ASTUndefined)
+    {
+      assert(nf != NULL);
+      alreadyWarned = false;
+      cache.push_back(Entry(SOLVER_UNDECIDED));
+      symbols.push_back(ASTVec());
+      print_success = false;
+    }
 
-       UserDefinedFlags& getUserFlags()
-       {
-               return bm.UserFlags;
-       }
+    const ASTVec
+    GetAsserts(void)
+    {
+      return bm.GetAsserts();
+    }
 
-       void AddAssert(const ASTNode& assert)
-       {
-               bm.AddAssert(assert);
-       }
+    UserDefinedFlags&
+    getUserFlags()
+    {
+      return bm.UserFlags;
+    }
 
-    void AddQuery(const ASTNode& q)
+    void
+    AddAssert(const ASTNode& assert)
     {
-       bm.AddQuery(q);
+      bm.AddAssert(assert);
     }
 
-       //NODES//
-    ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec)
+    void
+    AddQuery(const ASTNode& q)
     {
-        return nf->CreateNode(kind,children);
+      bm.AddQuery(q);
     }
 
-    ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTNode n0, const BEEV::ASTNode n1)
+    //NODES//
+    ASTNode
+    CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec)
     {
-        if (n0.GetIndexWidth() > 0 && !alreadyWarned)
-          {
-            cerr << "Warning: Parsing a term that uses array extensionality. STP doesn't handle array extensionality." << endl;
-            alreadyWarned = true;
-          }
-        return nf->CreateNode(kind,n0,n1);
+      return nf->CreateNode(kind, children);
     }
 
+    ASTNode
+    CreateNode(BEEV::Kind kind, const BEEV::ASTNode n0, const BEEV::ASTNode n1)
+    {
+      if (n0.GetIndexWidth() > 0 && !alreadyWarned)
+        {
+          cerr << "Warning: Parsing a term that uses array extensionality. STP doesn't handle array extensionality."
+              << endl;
+          alreadyWarned = true;
+        }
+      return nf->CreateNode(kind, n0, n1);
+    }
 
     // These belong in the node factory..
 
     //TERMS//
-    ASTNode CreateZeroConst(unsigned int width)
+    ASTNode
+    CreateZeroConst(unsigned int width)
     {
-       return bm.CreateZeroConst(width);
+      return bm.CreateZeroConst(width);
     }
 
-    ASTNode CreateOneConst(unsigned int width)
+    ASTNode
+    CreateOneConst(unsigned int width)
     {
-        return bm.CreateOneConst(width);
+      return bm.CreateOneConst(width);
     }
 
-    ASTNode CreateBVConst(string& strval, int base, int bit_width)
+    ASTNode
+    CreateBVConst(string& strval, int base, int bit_width)
     {
-       return bm.CreateBVConst(strval, base, bit_width);
+      return bm.CreateBVConst(strval, base, bit_width);
     }
 
-    ASTNode CreateBVConst(const char* const strval, int base)
+    ASTNode
+    CreateBVConst(const char* const strval, int base)
     {
-       return bm.CreateBVConst(strval, base);
+      return bm.CreateBVConst(strval, base);
     }
 
-    ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst)
+    ASTNode
+    CreateBVConst(unsigned int width, unsigned long long int bvconst)
     {
-       return bm.CreateBVConst(width, bvconst);
+      return bm.CreateBVConst(width, bvconst);
     }
 
-    ASTNode LookupOrCreateSymbol(const char * const name)
+    ASTNode
+    LookupOrCreateSymbol(const char * const name)
     {
-       return bm.LookupOrCreateSymbol(name);
+      return bm.LookupOrCreateSymbol(name);
     }
 
-    ASTNode LookupOrCreateSymbol(string name)
+    ASTNode
+    LookupOrCreateSymbol(string name)
     {
-       return bm.LookupOrCreateSymbol(name.c_str());
+      return bm.LookupOrCreateSymbol(name.c_str());
     }
 
-    bool LookupSymbol(const char * const name, ASTNode& output)
+    bool
+    LookupSymbol(const char * const name, ASTNode& output)
     {
-      return bm.LookupSymbol(name,output);
+      return bm.LookupSymbol(name, output);
     }
 
-    bool isSymbolAlreadyDeclared(char* name)
+    bool
+    isSymbolAlreadyDeclared(char* name)
     {
-           return bm.LookupSymbol(name);
+      return bm.LookupSymbol(name);
     }
 
-    void setPrintSuccess(bool ps)
+    void
+    setPrintSuccess(bool ps)
     {
-      print_success= ps;
+      print_success = ps;
     }
 
-
-    bool isSymbolAlreadyDeclared(string name)
-       {
-          return bm.LookupSymbol(name.c_str());
-       }
+    bool
+    isSymbolAlreadyDeclared(string name)
+    {
+      return bm.LookupSymbol(name.c_str());
+    }
 
     // Create the node, then "new" it.
-    ASTNode * newNode(const Kind k, const ASTNode& n0, const ASTNode& n1)
+    ASTNode *
+    newNode(const Kind k, const ASTNode& n0, const ASTNode& n1)
     {
-      return newNode(CreateNode(k,n0,n1));
+      return newNode(CreateNode(k, n0, n1));
     }
 
     // Create the node, then "new" it.
-    ASTNode * newNode(const Kind k, const int width, const ASTNode& n0, const ASTNode& n1)
+    ASTNode *
+    newNode(const Kind k, const int width, const ASTNode& n0, const ASTNode& n1)
     {
-      return newNode(nf->CreateTerm(k,width,n0,n1));
+      return newNode(nf->CreateTerm(k, width, n0, n1));
     }
 
-
     // On testcase20 it took about 4.2 seconds to parse using the standard allocator and the pool allocator.
-       ASTNode * newNode(const ASTNode& copyIn)
-       {
-               return new ASTNode(copyIn);
-               //return node_pool.construct(copyIn);
-       }
-
-       void deleteNode(ASTNode *n)
-       {
-               delete n;
-               //node_pool.destroy(n);
-       }
-
-       struct Entry
-       {
-         explicit Entry( SOLVER_RETURN_TYPE result_)
-         {
-           result = result_;
-         }
-
-         SOLVER_RETURN_TYPE result;
-         ASTNode node;
-
-         void print()
-         {
-            if (result == SOLVER_UNSATISFIABLE)
-              cerr << "u";
-            else if (result ==  SOLVER_SATISFIABLE)
-              cerr << "s";
-            else if (result ==  SOLVER_UNDECIDED)
-              cerr << "?";
-         }
-       };
-       vector<Entry> cache;
-       vector<vector<ASTNode> > symbols;
-
-       void
-       addSymbol(ASTNode &s)
-       {
-         symbols.back().push_back(s);
-         letMgr._parser_symbol_table.insert(s);
-       }
-
-       void
-        success()
-        {
-          if (print_success)
-            {
-              cout << "success" << endl;
-              flush(cout);
-            }
-        }
+    ASTNode *
+    newNode(const ASTNode& copyIn)
+    {
+      return new ASTNode(copyIn);
+      //return node_pool.construct(copyIn);
+    }
 
-        void
-        pop()
-        {
-          if (symbols.size() ==0)
-            FatalError("Popping from an empty stack.");
-          if (symbols.size() ==1)
-             FatalError("Can't pop away the default base element.");
-
-          assert(symbols.size() == cache.size());
-          cache.erase(cache.end()-1);
-          ASTVec & current = symbols.back();
-          for (int i=0; i < current.size() ;i++)
-              letMgr._parser_symbol_table.erase(current[i]);
-          symbols.erase(symbols.end()-1);
-        }
+    void
+    deleteNode(ASTNode *n)
+    {
+      delete n;
+      //node_pool.destroy(n);
+    }
+
+    struct Entry
+    {
+      explicit
+      Entry(SOLVER_RETURN_TYPE result_)
+      {
+        result = result_;
+      }
+
+      SOLVER_RETURN_TYPE result;
+      ASTNode node;
+
+      void
+      print()
+      {
+        if (result == SOLVER_UNSATISFIABLE)
+          cerr << "u";
+        else if (result == SOLVER_SATISFIABLE)
+          cerr << "s";
+        else if (result == SOLVER_UNDECIDED)
+          cerr << "?";
+      }
+    };
+    vector<Entry> cache;
+    vector<vector<ASTNode> > symbols;
 
-        void
-        push()
+    void
+    addSymbol(ASTNode &s)
+    {
+      symbols.back().push_back(s);
+      letMgr._parser_symbol_table.insert(s);
+    }
+
+    void
+    success()
+    {
+      if (print_success)
         {
-          // If the prior one is unsatisiable then the new one will be too.
-          if (cache.size() > 1 && cache.back().result == SOLVER_UNSATISFIABLE)
-            cache.push_back(Entry(SOLVER_UNSATISFIABLE));
-          else
-            cache.push_back(Entry(SOLVER_UNDECIDED));
-
-          symbols.push_back(ASTVec());
-          assert(symbols.size() == cache.size());
+          cout << "success" << endl;
+          flush(cout);
         }
+    }
 
-     void printStatus()
-     {
-      for (int i=0; i < cache.size();i++)
+    void
+    pop()
+    {
+      if (symbols.size() == 0)
+        FatalError("Popping from an empty stack.");
+      if (symbols.size() == 1)
+        FatalError("Can't pop away the default base element.");
+
+      assert(symbols.size() == cache.size());
+      cache.erase(cache.end() - 1);
+      ASTVec & current = symbols.back();
+      for (int i = 0; i < current.size(); i++)
+        letMgr._parser_symbol_table.erase(current[i]);
+      symbols.erase(symbols.end() - 1);
+    }
+
+    void
+    push()
+    {
+      // If the prior one is unsatisiable then the new one will be too.
+      if (cache.size() > 1 && cache.back().result == SOLVER_UNSATISFIABLE)
+        cache.push_back(Entry(SOLVER_UNSATISFIABLE));
+      else
+        cache.push_back(Entry(SOLVER_UNDECIDED));
+
+      symbols.push_back(ASTVec());
+      assert(symbols.size() == cache.size());
+    }
+
+    void
+    printStatus()
+    {
+      for (int i = 0; i < cache.size(); i++)
         {
           cache[i].print();
         }
-      cerr<< endl;
-     }
+      cerr << endl;
+    }
 
     void
     checkSat(vector<ASTVec> & assertionsSMT2);
 
-    void cleanUp()
+    void
+    cleanUp()
     {
       letMgr.cleanupParserSymbolTable();
       cache.clear();
       symbols.clear();
     }
-};
+  };
 }
 
 #endif /* PARSERINTERFACE_H_ */