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 7b33ae5cd17534f58065d59c1a72c23676de9076..5e619d240eed63caf6522a34087d773af3f1bb21 100644 (file)
--- 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 23aea2cd73daaac7980fec0006fcc5f7ac66afe6..f67589a21133bb2cece93842efea95df96dc1326 100644 (file)
--- 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 c28efaf9a776c03f18362a3df47c7c5252c37be0..bdcbdc6aaf85a2f1bf86a5a60b463003793a7a39 100644 (file)
--- 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 d71fd9bdfba76413d65e7f220142f1f2448211c3..459f0ed2ed97e53028c9dc832644f34427a91791 100644 (file)
--- 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 b6e34d9ded57e6f796f39bc68be01324b12f1b2b..ba813035ba3362050ca9a52e7e1c17a00f4338ac 100644 (file)
--- 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;
 }