emacs indentation done

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

diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp
index dae4a17de15e18ae13c6107e402ff865d052b855..945c3caab306372817babd4d05a469343b244b7b 100644 (file)
--- a/src/AST/AbstractionRefinement.cpp
+++ b/src/AST/AbstractionRefinement.cpp
@@ -204,7 +204,7 @@ namespace BEEV
   
   //Creates Array Write Axioms
   ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, 
-                                          const ASTNode& newvar)
+                                           const ASTNode& newvar)
   {
     if (READ != term.GetKind() && WRITE != term[0].GetKind())
       {
@@ -241,16 +241,16 @@ namespace BEEV
                                                                  const ASTNode& original_input)
   {
     for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),iend=GlobalList_Of_FiniteLoops.end();
-       i!=iend;i++)
+        i!=iend;i++)
       {
-       ASTNodeMap ParamToCurrentValMap;
-       SOLVER_RETURN_TYPE ret = SATBased_FiniteLoop_Refinement(SatSolver,
-                                                               original_input,
-                                                               *i,&ParamToCurrentValMap);
-       if(SOLVER_UNDECIDED != ret)
-         {
-           return ret;
-         }
+        ASTNodeMap ParamToCurrentValMap;
+        SOLVER_RETURN_TYPE ret = SATBased_FiniteLoop_Refinement(SatSolver,
+                                                                original_input,
+                                                                *i,&ParamToCurrentValMap);
+        if(SOLVER_UNDECIDED != ret)
+          {
+            return ret;
+          }
       }
     return SOLVER_UNDECIDED;
   } //end of SATBased_AllFiniteLoops_Refinement()

diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index 09397818f3a2dc44af05e36d786a89f82770ac16..74080730465e739e170a1f9112fd2c19e5ca01c0 100644 (file)
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -258,10 +258,10 @@ namespace BEEV
           break;
         }
       case FOR:
-       //Insert in a global list of FOR constructs. Return TRUE now
-       bm.GlobalList_Of_FiniteLoops.push_back(simpleForm);
-       return bm.CreateNode(TRUE);
-       break;
+        //Insert in a global list of FOR constructs. Return TRUE now
+        bm.GlobalList_Of_FiniteLoops.push_back(simpleForm);
+        return bm.CreateNode(TRUE);
+        break;
       default:
         if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType())
           result = simpleForm;

diff --git a/src/main/main.cpp b/src/main/main.cpp
index d1b9f19d2a646a2dfca5c5163fda2aad7e736c8c..86da6869e628ce277605032fcd51b764a462e766 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -188,13 +188,13 @@ int main(int argc, char ** argv) {
   if(print_STPinput_back_flag) 
     {
       if(smtlib_parser_flag) 
-       {
-         FatalError("Print back feature for SMT format not yet implemented\n");
-       }
+        {
+          FatalError("Print back feature for SMT format not yet implemented\n");
+        }
       else 
-       {
-         print_STPInput_Back(asserts, query);
-       }
+        {
+          print_STPInput_Back(asserts, query);
+        }
       return 0;
     } //end of PrintBack if
 

diff --git a/src/parser/let-funcs.cpp b/src/parser/let-funcs.cpp
index fc45b30fb2ca7b44a48b0776b9f686b94b907e52..c14de07ae399a5e88b678391ecb7b608b03a8022 100644 (file)
--- a/src/parser/let-funcs.cpp
+++ b/src/parser/let-funcs.cpp
@@ -30,12 +30,12 @@ namespace BEEV {
     if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && 
        it->second != ASTUndefined) {      
       FatalError("LetExprMgr:The LET-var v has already been defined"\
-                "in this LET scope: v =", var);
+                 "in this LET scope: v =", var);
     }
 
     if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) {
       FatalError("LetExprMgr:This var is already declared. "\
-                "cannot redeclare as a letvar: v =", var);
+                 "cannot redeclare as a letvar: v =", var);
     }
 
     (*_letid_expr_map)[var] = letExpr;   

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index aeea77b9f26c850709738d8e74daee9f21b7ac35..ef0d637ec4cc1bd94cb187235517a6c25fe11562 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -47,10 +47,10 @@ namespace BEEV
     if (pushNeg && (it = SimplifyMap->find(key)) != SimplifyMap->end())
       {
         output = 
-         (ASTFalse == it->second) ? 
-         ASTTrue : 
-         (ASTTrue == it->second) ? 
-         ASTFalse : CreateNode(NOT, it->second);
+          (ASTFalse == it->second) ? 
+          ASTTrue : 
+          (ASTTrue == it->second) ? 
+          ASTFalse : CreateNode(NOT, it->second);
         CountersAndStats("2nd_Successful_CheckSimplifyMap");
         return true;
       }