From: Andres Notzli <andres.noetzli@gmail.com>
Date: Thu, 4 Aug 2016 22:12:54 +0000 (-0700)
Subject: Minor: add/fix comments, remove redundant includes
X-Git-Tag: cvc5-1.0.0~6040^2~12^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0812bb7f36c454d282be5e9960a9a820e4fbd52c;p=cvc5.git

Minor: add/fix comments, remove redundant includes
---

diff --git a/proofs/signatures/th_arrays.plf b/proofs/signatures/th_arrays.plf
index b54a4ed5b..acfbd2f3b 100755
--- 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 23d7d1972..cb5a2bdd1 100644
--- 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 80a737580..34248f7eb 100644
--- 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;