From e5f5e008aaa6e090771a08f9cc666eaecb64631a Mon Sep 17 00:00:00 2001 From: Kenneth McMillan Date: Sun, 3 Mar 2013 21:22:50 -0800 Subject: [PATCH] fixing file heads to match z3 --- src/interp/foci2.h | 19 +++++++++++++++++++ src/interp/iz3base.cpp | 21 ++++++++++++++++++++- src/interp/iz3base.h | 20 +++++++++++++++++++- src/interp/iz3foci.cpp | 19 ++++++++++++++++++- src/interp/iz3foci.h | 19 ++++++++++++++++++- src/interp/iz3hash.h | 18 ++++++++++++++++++ src/interp/iz3mgr.cpp | 19 ++++++++++++++++++- src/interp/iz3mgr.h | 19 ++++++++++++++++++- src/interp/iz3profiling.h | 19 ++++++++++++++++++- src/interp/iz3proof.cpp | 20 +++++++++++++++++++- src/interp/iz3proof.h | 19 ++++++++++++++++++- src/interp/iz3scopes.cpp | 19 ++++++++++++++++++- src/interp/iz3scopes.h | 20 +++++++++++++++++++- src/interp/iz3secondary.h | 20 +++++++++++++++++++- 14 files changed, 259 insertions(+), 12 deletions(-) diff --git a/src/interp/foci2.h b/src/interp/foci2.h index 3f32b8118..261dd05dc 100755 --- a/src/interp/foci2.h +++ b/src/interp/foci2.h @@ -1,3 +1,22 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + foci2.h + +Abstract: + + An interface class for foci2. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + #ifndef FOCI2_H #define FOCI2_H diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index 44006f7f2..d3b469462 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -1,4 +1,23 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3base.cpp + +Abstract: + + Base class for interpolators. Includes an AST manager and a scoping + object as bases. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + #include "iz3base.h" #include diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 383a89ea4..4209f3c67 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -1,4 +1,22 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3base.h + +Abstract: + + Base class for interpolators. Includes an AST manager and a scoping + object as bases. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #ifndef IZ3BASE_H #define IZ3BASE_H diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index 741391a8d..31d8b56c7 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -1,4 +1,21 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3foci.cpp + +Abstract: + + Implements a secondary solver using foci2. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #include #include diff --git a/src/interp/iz3foci.h b/src/interp/iz3foci.h index 4b7040b98..86b049f24 100755 --- a/src/interp/iz3foci.h +++ b/src/interp/iz3foci.h @@ -1,4 +1,21 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3foci.h + +Abstract: + + Implements a secondary solver using foci2. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #ifndef IZ3FOCI_H #define IZ3FOCI_H diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index abbe5b5fb..f6767c037 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -1,3 +1,21 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3hash.h + +Abstract: + + Wrapper for stl hash tables + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ // pull in the headers for has_map and hash_set // these live in non-standard places diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index b79fa0f6b..b1f07f5ce 100644 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -1,4 +1,21 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3mgr.cpp + +Abstract: + + A wrapper around an ast manager, providing convenience methods. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #include "iz3mgr.h" diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 211b9a45a..32ec25d70 100644 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -1,4 +1,21 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3mgr.h + +Abstract: + + A wrapper around an ast manager, providing convenience methods. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #ifndef IZ3MGR_H #define IZ3MGR_H diff --git a/src/interp/iz3profiling.h b/src/interp/iz3profiling.h index fd518b1d9..cdb7066e3 100755 --- a/src/interp/iz3profiling.h +++ b/src/interp/iz3profiling.h @@ -1,4 +1,21 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3profiling.h + +Abstract: + + Some routines for measuring performance. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #ifndef IZ3PROFILING_H #define IZ3PROFILING_H diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp index 4c79a4ae6..968a4b25a 100755 --- a/src/interp/iz3proof.cpp +++ b/src/interp/iz3proof.cpp @@ -1,4 +1,22 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3proof.cpp + +Abstract: + + This class defines a simple interpolating proof system. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + #include "iz3proof.h" diff --git a/src/interp/iz3proof.h b/src/interp/iz3proof.h index ea1973f63..ae08e9d36 100755 --- a/src/interp/iz3proof.h +++ b/src/interp/iz3proof.h @@ -1,4 +1,21 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3proof.h + +Abstract: + + This class defines a simple interpolating proof system. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #ifndef IZ3PROOF_H #define IZ3PROOF_H diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp index 65c6f6d88..90ff3b829 100755 --- a/src/interp/iz3scopes.cpp +++ b/src/interp/iz3scopes.cpp @@ -1,4 +1,21 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3scopes.cpp + +Abstract: + + Calculations with scopes, for both sequence and tree interpolation. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ #include diff --git a/src/interp/iz3scopes.h b/src/interp/iz3scopes.h index e7ca387d5..2ba3a999f 100755 --- a/src/interp/iz3scopes.h +++ b/src/interp/iz3scopes.h @@ -1,4 +1,22 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3scopes.h + +Abstract: + + Calculations with scopes, for both sequence and tree interpolation. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + #ifndef IZ3SOPES_H #define IZ3SOPES_H diff --git a/src/interp/iz3secondary.h b/src/interp/iz3secondary.h index 749feaacc..0eb1b9a93 100755 --- a/src/interp/iz3secondary.h +++ b/src/interp/iz3secondary.h @@ -1,4 +1,22 @@ -/* Copyright 2011 Microsoft Research. */ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + iz3secondary + +Abstract: + + Interface for secondary provers. + +Author: + + Ken McMillan (kenmcmil) + +Revision History: + +--*/ + #ifndef IZ3SECONDARY_H #define IZ3SECONDARY_H