Minor: add/fix comments, remove redundant includes

diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index b54a4ed5bd97807113e8696d0d2ac32cf7a5dd3b..acfbd2f3b29669ab218c234e69bc1d96cdc8bbf3 100755 (executable)
--- a/proofs/signatures/th_arrays.plf
+++ b/proofs/signatures/th_arrays.plf
@@ -32,6 +32,7 @@
                (th_holds (= _
                (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) t3))))))))
 
+; read( a[i] = b, j ) == read( a, j ) if i != j
 (declare row (! s1 sort
              (! s2 sort
              (! t2 (term s1)
@@ -42,6 +43,7 @@
                (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3)
                                      (apply _ _ (apply _ _ (read s1 s2) t1) t3)))))))))))
 
+; i == j if read( a, j ) != read( a[i] = b, j )
 (declare negativerow (! s1 sort
                      (! s2 sort
                      (! t2 (term s1)
@@ -60,4 +62,4 @@
              (! u1 (! k (term s1)
                    (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k)))))
                      (holds cln)))
-               (holds cln)))))))
\ No newline at end of file
+               (holds cln)))))))

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 23d7d19727072028ee827b42a63df1082cfab347..cb5a2bdd17405c61ca98565c65804a66f5d9f67c 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -21,13 +21,11 @@
 
 #include <iosfwd>
 #include <map>
-#include "proof/proof.h"
-#include "proof/proof_utils.h"
-#include "proof/skolemization_manager.h"
-#include "util/proof.h"
 #include "expr/node.h"
 #include "proof/clause_id.h"
 #include "proof/proof.h"
+#include "proof/proof_utils.h"
+#include "proof/skolemization_manager.h"
 #include "theory/logic_info.h"
 #include "theory/substitutions.h"
 #include "util/proof.h"

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 80a737580206c498c986f56f422aa3a114444069..34248f7ebdc05d4f8e1d1d60d35b971eb00e949f 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -205,7 +205,7 @@ public:
   {}
   virtual ~TheoryProof() {};
   /**
-   * Print a term belonging some theory, not neccessarily this one.
+   * Print a term belonging some theory, not necessarily this one.
    *
    * @param term expresion representing term
    * @param os output stream
@@ -216,7 +216,7 @@ public:
   /**
    * Print a term belonging to THIS theory.
    *
-   * @param term expresion representing term
+   * @param term expression representing term
    * @param os output stream
    */
   virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;