From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 31 Aug 2009 19:40:25 +0000 (+0000)
Subject: minor edits
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2e662deed02e8b5d484957689974c39642422b63;p=francis%2Fstp.git

minor edits

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

diff --git a/README b/README
index 7b33ae5..5e619d2 100644
--- a/README
+++ b/README
@@ -26,10 +26,10 @@ http://sourceforge.net/projects/stp-fast-prover
 
 DOCUMENTATION
 -------------
-http://people.csail.mit.edu/vganesh/STP_files/stp-docs.html
+http://sites.google.com/site/stpfastprover
 
 
 PAPERS
 -----
-http://people.csail.mit.edu/vganesh/STP_files/stp-papers.html
+http://sites.google.com/site/stpfastprover
 
diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp
index 23aea2c..f67589a 100644
--- a/src/AST/AST.cpp
+++ b/src/AST/AST.cpp
@@ -841,8 +841,8 @@ bool BeevMgr::BVTypeCheckRecursive(const ASTNode& n)
  * typecheck as you go along. It is not suitable as a general
  * typechecker.
  *
- * If this returns, this ALWAYS returns true. If there is an error it will call
- * FatalError() and abort.
+ * If this returns, this ALWAYS returns true. If there is an error it
+ * will call FatalError() and abort.
  */
 
 
@@ -1051,6 +1051,9 @@ bool BeevMgr::BVTypeCheck(const ASTNode& n)
 				if (3 != n.Degree())
 					FatalError("BVTypeCheck:ITE must have exactly 3 ChildNodes", n);
 				break;
+		        case FOR:
+			  //FIXME: Todo
+			        break;
 			default:
 				FatalError("BVTypeCheck: Unrecognized kind: ", ASTUndefined);
 				break;
diff --git a/src/AST/AST.h b/src/AST/AST.h
index c28efaf..bdcbdc6 100644
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -1692,6 +1692,7 @@ public:
 	ASTNode TransformFormula(const ASTNode& query);
 	ASTNode TransformTerm(const ASTNode& term);
 	ASTNode TransformArray(const ASTNode& term);
+	ASTNode TransformFiniteFor(const ASTNode& form);
 	ASTNode TranslateSignedDivModRem(const ASTNode& term);
 	void    assertTransformPostConditions(const ASTNode & term);
 
diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index d71fd9b..459f0ed 100644
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -577,4 +577,10 @@ ASTNode BeevMgr::TransformArray(const ASTNode& term)
 	TransformMap[term] = result;
 	return result;
 } //end of TransformArray()
+
+ASTNode BeevMgr::TransformFiniteFor(const ASTNode& form)
+{
+  return form;
+}
+
 } //end of namespace BEEV
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index b6e34d9..ba81303 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -276,7 +276,7 @@ ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg)
 }
 
 ASTNode BeevMgr::SimplifyForFormula(const ASTNode& a, bool pushNeg) {
-        //Code this up properly later. Mainly pushing the negation down
+        //FIXME: Code this up properly later. Mainly pushing the negation down
         return a;
 }