From b08ccc7816978ce17637ff446dbfa1e3dd9e365d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Jun 2015 11:54:02 -0700 Subject: [PATCH] added missing Copyright forms Signed-off-by: Nikolaj Bjorner --- scripts/mk_copyright.py | 54 +++++++++++++++++++++++ src/api/dll/dll.cpp | 6 +++ src/api/z3_api.h | 6 +++ src/api/z3_macros.h | 6 +++ src/ast/proof_checker/proof_checker.cpp | 6 +++ src/ast/simplifier/bv_elim.cpp | 6 +++ src/muz/base/dl_boogie_proof.cpp | 6 +++ src/muz/base/dl_boogie_proof.h | 6 +++ src/muz/base/hnf.h | 6 +++ src/muz/base/proof_utils.cpp | 6 +++ src/muz/fp/datalog_parser.cpp | 6 +++ src/muz/rel/check_relation.cpp | 6 +++ src/muz/rel/karr_relation.cpp | 6 +++ src/parsers/smt/smtlib.cpp | 6 +++ src/qe/nlarith_util.cpp | 6 +++ src/qe/qe_arith.h | 6 +++ src/qe/qe_array_plugin.cpp | 6 +++ src/qe/qe_cmd.cpp | 6 +++ src/qe/qe_datatype_plugin.cpp | 6 +++ src/qe/qe_dl_plugin.cpp | 6 +++ src/qe/qe_util.cpp | 6 +++ src/shell/opt_frontend.cpp | 6 +++ src/shell/options.h | 6 +++ src/smt/database.h | 6 +++ src/tactic/arith/arith_bounds_tactic.cpp | 6 +++ src/test/api.cpp | 6 +++ src/test/api_bug.cpp | 6 +++ src/test/arith_rewriter.cpp | 6 +++ src/test/arith_simplifier_plugin.cpp | 6 +++ src/test/bits.cpp | 6 +++ src/test/bv_simplifier_plugin.cpp | 6 +++ src/test/check_assumptions.cpp | 6 +++ src/test/datalog_parser.cpp | 6 +++ src/test/ddnf.cpp | 6 +++ src/test/dl_context.cpp | 6 +++ src/test/dl_product_relation.cpp | 6 +++ src/test/dl_query.cpp | 6 +++ src/test/dl_relation.cpp | 6 +++ src/test/dl_table.cpp | 6 +++ src/test/dl_util.cpp | 6 +++ src/test/doc.cpp | 6 +++ src/test/expr_rand.cpp | 6 +++ src/test/expr_substitution.cpp | 6 +++ src/test/factor_rewriter.cpp | 6 +++ src/test/fuzzing/expr_delta.cpp | 6 +++ src/test/fuzzing/expr_rand.cpp | 6 +++ src/test/get_implied_equalities.cpp | 6 +++ src/test/heap_trie.cpp | 6 +++ src/test/hilbert_basis.cpp | 6 +++ src/test/horn_subsume_model_converter.cpp | 6 +++ src/test/karr.cpp | 6 +++ src/test/memory.cpp | 6 +++ src/test/model2expr.cpp | 6 +++ src/test/model_retrieval.cpp | 6 +++ src/test/nlarith_util.cpp | 6 +++ src/test/pdr.cpp | 6 +++ src/test/polynorm.cpp | 6 +++ src/test/proof_checker.cpp | 6 +++ src/test/qe_arith.cpp | 6 +++ src/test/quant_elim.cpp | 6 +++ src/test/quant_solve.cpp | 6 +++ src/test/sat_user_scope.cpp | 6 +++ src/test/simplex.cpp | 6 +++ src/test/simplifier.cpp | 6 +++ src/test/small_object_allocator.cpp | 6 +++ src/test/smt2print_parse.cpp | 6 +++ src/test/smt_context.cpp | 6 +++ src/test/sorting_network.cpp | 6 +++ src/test/substitution.cpp | 6 +++ src/test/tbv.cpp | 6 +++ src/test/test_util.h | 6 +++ src/test/theory_dl.cpp | 6 +++ src/test/theory_pb.cpp | 6 +++ src/test/timeout.cpp | 6 +++ src/test/udoc_relation.cpp | 6 +++ src/util/memory_manager.cpp | 6 +++ 76 files changed, 504 insertions(+) create mode 100644 scripts/mk_copyright.py diff --git a/scripts/mk_copyright.py b/scripts/mk_copyright.py new file mode 100644 index 000000000..f7a4cb8fd --- /dev/null +++ b/scripts/mk_copyright.py @@ -0,0 +1,54 @@ +import os +import re + +cr = re.compile("Copyright") +aut = re.compile("Automatically generated") + +cr_notice = """ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + +""" + +def has_cr(file): + ins = open(file) + lines = 0 + line = ins.readline() + while line and lines < 20: + m = cr.search(line) + if m: + ins.close() + return True + m = aut.search(line) + if m: + ins.close() + return True + line = ins.readline() + ins.close() + return False + +def add_cr(file): + tmp = "%s.tmp" % file + ins = open(file) + ous = open(tmp,'w') + ous.write(cr_notice) + line = ins.readline() + while line: + ous.write(line) + line = ins.readline() + ins.close() + ous.close() + os.system("move %s %s" % (tmp, file)) + +def add_missing_cr(): + for root, dirs, files in os.walk('src'): + for f in files: + if f.endswith('.cpp') or f.endswith('.h'): + path = "%s\\%s" % (root, f) + if not has_cr(path): + print "Missing CR for %s" % path + add_cr(path) + +add_missing_cr() diff --git a/src/api/dll/dll.cpp b/src/api/dll/dll.cpp index 1730ede23..a0bd25d2e 100644 --- a/src/api/dll/dll.cpp +++ b/src/api/dll/dll.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifdef _WINDOWS #include diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 4746d4a33..dfad8b755 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifndef _Z3_API_H_ #define _Z3_API_H_ diff --git a/src/api/z3_macros.h b/src/api/z3_macros.h index 7a0b6857c..cdac41c97 100644 --- a/src/api/z3_macros.h +++ b/src/api/z3_macros.h @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifndef __in #define __in #endif diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 41c43b26c..16546db1e 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "proof_checker.h" #include "ast_ll_pp.h" #include "ast_pp.h" diff --git a/src/ast/simplifier/bv_elim.cpp b/src/ast/simplifier/bv_elim.cpp index fc4e7534b..8dc2671ca 100644 --- a/src/ast/simplifier/bv_elim.cpp +++ b/src/ast/simplifier/bv_elim.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "bv_elim.h" #include "bv_decl_plugin.h" #include "var_subst.h" diff --git a/src/muz/base/dl_boogie_proof.cpp b/src/muz/base/dl_boogie_proof.cpp index 42d21dfb9..cc0e28e2a 100644 --- a/src/muz/base/dl_boogie_proof.cpp +++ b/src/muz/base/dl_boogie_proof.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + /** Example from Boogie: diff --git a/src/muz/base/dl_boogie_proof.h b/src/muz/base/dl_boogie_proof.h index 6c8fbbae3..0f829dbdf 100644 --- a/src/muz/base/dl_boogie_proof.h +++ b/src/muz/base/dl_boogie_proof.h @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + /** output :: derivation model diff --git a/src/muz/base/hnf.h b/src/muz/base/hnf.h index 9dc7cccd9..4d3edcb68 100644 --- a/src/muz/base/hnf.h +++ b/src/muz/base/hnf.h @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + /*-- Module Name: diff --git a/src/muz/base/proof_utils.cpp b/src/muz/base/proof_utils.cpp index d4a8ab22b..4bfbf3365 100644 --- a/src/muz/base/proof_utils.cpp +++ b/src/muz/base/proof_utils.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "dl_util.h" #include "proof_utils.h" #include "ast_smt2_pp.h" diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 58bc79e7a..c6f594d4e 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include"datalog_parser.h" #include"string_buffer.h" #include"str_hashtable.h" diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index 20364d5d5..60ca6c0be 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "check_relation.h" #include "dl_relation_manager.h" #include "qe_util.h" diff --git a/src/muz/rel/karr_relation.cpp b/src/muz/rel/karr_relation.cpp index 436cd8598..6b9126161 100644 --- a/src/muz/rel/karr_relation.cpp +++ b/src/muz/rel/karr_relation.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "karr_relation.h" #include "bool_rewriter.h" diff --git a/src/parsers/smt/smtlib.cpp b/src/parsers/smt/smtlib.cpp index d53d3cafa..b743b5b0f 100644 --- a/src/parsers/smt/smtlib.cpp +++ b/src/parsers/smt/smtlib.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include"smtlib.h" #include"ast_pp.h" #include"ast_smt2_pp.h" diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index c555b71f1..b7c1aef5d 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "ast.h" #include "nlarith_util.h" #include "arith_decl_plugin.h" diff --git a/src/qe/qe_arith.h b/src/qe/qe_arith.h index c8f7e8b8d..725245fad 100644 --- a/src/qe/qe_arith.h +++ b/src/qe/qe_arith.h @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #ifndef __QE_ARITH_H_ #define __QE_ARITH_H_ diff --git a/src/qe/qe_array_plugin.cpp b/src/qe/qe_array_plugin.cpp index c9de1d745..e7cbe65b9 100644 --- a/src/qe/qe_array_plugin.cpp +++ b/src/qe/qe_array_plugin.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include "qe.h" #include "array_decl_plugin.h" #include "expr_safe_replace.h" diff --git a/src/qe/qe_cmd.cpp b/src/qe/qe_cmd.cpp index 6f001c9da..9144c708c 100644 --- a/src/qe/qe_cmd.cpp +++ b/src/qe/qe_cmd.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "qe_cmd.h" #include "qe.h" #include "cmd_context.h" diff --git a/src/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp index 9b77de42a..088d2252d 100644 --- a/src/qe/qe_datatype_plugin.cpp +++ b/src/qe/qe_datatype_plugin.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + // --------------------- // datatypes // Quantifier elimination routine for recursive data-types. diff --git a/src/qe/qe_dl_plugin.cpp b/src/qe/qe_dl_plugin.cpp index a93301b4f..e04f4cbde 100644 --- a/src/qe/qe_dl_plugin.cpp +++ b/src/qe/qe_dl_plugin.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include "qe.h" #include "expr_safe_replace.h" #include "dl_decl_plugin.h" diff --git a/src/qe/qe_util.cpp b/src/qe/qe_util.cpp index 77396ac49..2cf723c08 100644 --- a/src/qe/qe_util.cpp +++ b/src/qe/qe_util.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "qe_util.h" #include "bool_rewriter.h" diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index 6e39313fd..78d083e6e 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include #include #include diff --git a/src/shell/options.h b/src/shell/options.h index 951062ff0..ee1de00fb 100644 --- a/src/shell/options.h +++ b/src/shell/options.h @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + /** \page cmdline Command line options diff --git a/src/smt/database.h b/src/smt/database.h index 69843f434..3edb87f1f 100644 --- a/src/smt/database.h +++ b/src/smt/database.h @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + static char const g_pattern_database[] = "(benchmark patterns \n" " :status unknown \n" diff --git a/src/tactic/arith/arith_bounds_tactic.cpp b/src/tactic/arith/arith_bounds_tactic.cpp index dc24a625b..83b5c6daf 100644 --- a/src/tactic/arith/arith_bounds_tactic.cpp +++ b/src/tactic/arith/arith_bounds_tactic.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include"arith_bounds_tactic.h" #include"arith_decl_plugin.h" diff --git a/src/test/api.cpp b/src/test/api.cpp index 234d1192c..a463bbe47 100644 --- a/src/test/api.cpp +++ b/src/test/api.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifdef _WINDOWS #include "z3.h" #include "z3_private.h" diff --git a/src/test/api_bug.cpp b/src/test/api_bug.cpp index 4519b2352..b88840eb6 100644 --- a/src/test/api_bug.cpp +++ b/src/test/api_bug.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include #include"z3.h" diff --git a/src/test/arith_rewriter.cpp b/src/test/arith_rewriter.cpp index 9eb9e559b..5ed7c3501 100644 --- a/src/test/arith_rewriter.cpp +++ b/src/test/arith_rewriter.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "arith_rewriter.h" #include "bv_decl_plugin.h" #include "ast_pp.h" diff --git a/src/test/arith_simplifier_plugin.cpp b/src/test/arith_simplifier_plugin.cpp index 59f4996ce..8464fd830 100644 --- a/src/test/arith_simplifier_plugin.cpp +++ b/src/test/arith_simplifier_plugin.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "arith_eq_solver.h" #include "smt_params.h" diff --git a/src/test/bits.cpp b/src/test/bits.cpp index 7254a177d..f32871a5a 100644 --- a/src/test/bits.cpp +++ b/src/test/bits.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + // Test some bit hacks #include"util.h" #include"debug.h" diff --git a/src/test/bv_simplifier_plugin.cpp b/src/test/bv_simplifier_plugin.cpp index 77e57f1f5..dc930bb82 100644 --- a/src/test/bv_simplifier_plugin.cpp +++ b/src/test/bv_simplifier_plugin.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "bv_simplifier_plugin.h" #include "arith_decl_plugin.h" #include "ast_pp.h" diff --git a/src/test/check_assumptions.cpp b/src/test/check_assumptions.cpp index 872af714c..fa8327cd4 100644 --- a/src/test/check_assumptions.cpp +++ b/src/test/check_assumptions.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "memory_manager.h" #include "smt_params.h" #include "ast.h" diff --git a/src/test/datalog_parser.cpp b/src/test/datalog_parser.cpp index e23650e3b..a927be29a 100644 --- a/src/test/datalog_parser.cpp +++ b/src/test/datalog_parser.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "datalog_parser.h" #include "ast_pp.h" #include "arith_decl_plugin.h" diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index 024f1bb0f..8620bd441 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "ddnf.h" #include "tbv.h" #include diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp index 5c70aa8b5..09db4bde2 100644 --- a/src/test/dl_context.cpp +++ b/src/test/dl_context.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "datalog_parser.h" #include "ast_pp.h" #include "arith_decl_plugin.h" diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp index 357ccd604..c375587fb 100644 --- a/src/test/dl_product_relation.cpp +++ b/src/test/dl_product_relation.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifdef _WINDOWS #include "dl_context.h" #include "dl_register_engine.h" diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp index 39ea06959..9e0f285c7 100644 --- a/src/test/dl_query.cpp +++ b/src/test/dl_query.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "datalog_parser.h" #include "ast_pp.h" #include "dl_table_relation.h" diff --git a/src/test/dl_relation.cpp b/src/test/dl_relation.cpp index bb1c8614c..c2ce807a9 100644 --- a/src/test/dl_relation.cpp +++ b/src/test/dl_relation.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifdef _WINDOWS #include "dl_context.h" #include "dl_register_engine.h" diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp index d24200f9b..6dc688ede 100644 --- a/src/test/dl_table.cpp +++ b/src/test/dl_table.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifdef _WINDOWS #include "dl_context.h" #include "dl_table.h" diff --git a/src/test/dl_util.cpp b/src/test/dl_util.cpp index 601fd630a..02e40bbd9 100644 --- a/src/test/dl_util.cpp +++ b/src/test/dl_util.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "dl_util.h" using namespace datalog; diff --git a/src/test/doc.cpp b/src/test/doc.cpp index 593d09cfe..b2863a629 100644 --- a/src/test/doc.cpp +++ b/src/test/doc.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "doc.h" #include "trace.h" #include "vector.h" diff --git a/src/test/expr_rand.cpp b/src/test/expr_rand.cpp index 19a07e98a..972c6e242 100644 --- a/src/test/expr_rand.cpp +++ b/src/test/expr_rand.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "expr_rand.h" #include "ast_pp.h" #include "bv_decl_plugin.h" diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp index f83bde97d..8af3f7197 100644 --- a/src/test/expr_substitution.cpp +++ b/src/test/expr_substitution.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "expr_substitution.h" #include "smt_params.h" #include "substitution.h" diff --git a/src/test/factor_rewriter.cpp b/src/test/factor_rewriter.cpp index 625710fe1..3bcdcd9e9 100644 --- a/src/test/factor_rewriter.cpp +++ b/src/test/factor_rewriter.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "factor_rewriter.h" #include "bv_decl_plugin.h" #include "ast_pp.h" diff --git a/src/test/fuzzing/expr_delta.cpp b/src/test/fuzzing/expr_delta.cpp index 344e555c9..fd5117a74 100644 --- a/src/test/fuzzing/expr_delta.cpp +++ b/src/test/fuzzing/expr_delta.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "expr_delta.h" #include "ast_pp.h" diff --git a/src/test/fuzzing/expr_rand.cpp b/src/test/fuzzing/expr_rand.cpp index a2aca7e6e..f56704e45 100644 --- a/src/test/fuzzing/expr_rand.cpp +++ b/src/test/fuzzing/expr_rand.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "expr_rand.h" #include "bv_decl_plugin.h" #include "array_decl_plugin.h" diff --git a/src/test/get_implied_equalities.cpp b/src/test/get_implied_equalities.cpp index 2576920cc..37fbe2004 100644 --- a/src/test/get_implied_equalities.cpp +++ b/src/test/get_implied_equalities.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "z3.h" #include "trace.h" #include "debug.h" diff --git a/src/test/heap_trie.cpp b/src/test/heap_trie.cpp index 92ef97f72..5b0047e82 100644 --- a/src/test/heap_trie.cpp +++ b/src/test/heap_trie.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "heap_trie.h" struct unsigned_le { diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index 6fdfb1560..57c8c5050 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "hilbert_basis.h" #include "ast_pp.h" #include "reg_decl_plugins.h" diff --git a/src/test/horn_subsume_model_converter.cpp b/src/test/horn_subsume_model_converter.cpp index 28359b954..4b653e3a8 100644 --- a/src/test/horn_subsume_model_converter.cpp +++ b/src/test/horn_subsume_model_converter.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include "horn_subsume_model_converter.h" #include "arith_decl_plugin.h" #include "model_smt2_pp.h" diff --git a/src/test/karr.cpp b/src/test/karr.cpp index 87debf662..4c0737230 100644 --- a/src/test/karr.cpp +++ b/src/test/karr.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "hilbert_basis.h" /* diff --git a/src/test/memory.cpp b/src/test/memory.cpp index 0f5a92e2c..340a1929c 100644 --- a/src/test/memory.cpp +++ b/src/test/memory.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifdef _WINDOWS #include "z3.h" #include "z3_private.h" diff --git a/src/test/model2expr.cpp b/src/test/model2expr.cpp index abca706c1..f96cee55f 100644 --- a/src/test/model2expr.cpp +++ b/src/test/model2expr.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "model2expr.h" #include "ast_pp.h" #include "arith_decl_plugin.h" diff --git a/src/test/model_retrieval.cpp b/src/test/model_retrieval.cpp index f40f89d22..e42e22539 100644 --- a/src/test/model_retrieval.cpp +++ b/src/test/model_retrieval.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include "ast.h" #include "smt_params.h" #include "smt_context.h" diff --git a/src/test/nlarith_util.cpp b/src/test/nlarith_util.cpp index f08fa020e..2def66b38 100644 --- a/src/test/nlarith_util.cpp +++ b/src/test/nlarith_util.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "nlarith_util.h" #include "arith_decl_plugin.h" #include "ast_pp.h" diff --git a/src/test/pdr.cpp b/src/test/pdr.cpp index a9194ec60..a1410b482 100644 --- a/src/test/pdr.cpp +++ b/src/test/pdr.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "pdr_context.h" #include "reg_decl_plugins.h" diff --git a/src/test/polynorm.cpp b/src/test/polynorm.cpp index 3593e98ce..a8f4ab861 100644 --- a/src/test/polynorm.cpp +++ b/src/test/polynorm.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "th_rewriter.h" #include "smt2parser.h" #include "arith_decl_plugin.h" diff --git a/src/test/proof_checker.cpp b/src/test/proof_checker.cpp index 12a5245e6..7f9827187 100644 --- a/src/test/proof_checker.cpp +++ b/src/test/proof_checker.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "proof_checker.h" #include "ast_ll_pp.h" diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp index 8b6577b3f..bd8266dc2 100644 --- a/src/test/qe_arith.cpp +++ b/src/test/qe_arith.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "qe_arith.h" #include "qe.h" #include "th_rewriter.h" diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp index 15d23a574..0fe7f8eec 100644 --- a/src/test/quant_elim.cpp +++ b/src/test/quant_elim.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "ast.h" #include "smt_params.h" #include "simplifier.h" diff --git a/src/test/quant_solve.cpp b/src/test/quant_solve.cpp index ae2dadee9..aa1306128 100644 --- a/src/test/quant_solve.cpp +++ b/src/test/quant_solve.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "ast.h" #include "smt_params.h" #include "qe.h" diff --git a/src/test/sat_user_scope.cpp b/src/test/sat_user_scope.cpp index e39059563..5107361bd 100644 --- a/src/test/sat_user_scope.cpp +++ b/src/test/sat_user_scope.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "sat_solver.h" #include "util.h" diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp index a70d0d8cf..61ab7180b 100644 --- a/src/test/simplex.cpp +++ b/src/test/simplex.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "sparse_matrix.h" #include "sparse_matrix_def.h" #include "simplex.h" diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp index 733c9e23a..2e8f434e1 100644 --- a/src/test/simplifier.cpp +++ b/src/test/simplifier.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #ifdef _WINDOWS #include "z3.h" #include "z3_private.h" diff --git a/src/test/small_object_allocator.cpp b/src/test/small_object_allocator.cpp index 1e74a734b..1ecf865dd 100644 --- a/src/test/small_object_allocator.cpp +++ b/src/test/small_object_allocator.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include #include"util.h" #include"trace.h" diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 39543d141..982e2e3f5 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + // This is to test the print-parse facilities over the API // for SMT-LIB2. diff --git a/src/test/smt_context.cpp b/src/test/smt_context.cpp index 49ada8ebd..6c44b8b1d 100644 --- a/src/test/smt_context.cpp +++ b/src/test/smt_context.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "smt_context.h" #include "reg_decl_plugins.h" diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index dd46b61df..4802e2bec 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "trace.h" #include "vector.h" #include "ast.h" diff --git a/src/test/substitution.cpp b/src/test/substitution.cpp index 0d7fb5856..cdc7f2080 100644 --- a/src/test/substitution.cpp +++ b/src/test/substitution.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "expr_substitution.h" #include "smt_params.h" #include "substitution.h" diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index c53eb3671..7637c7e83 100644 --- a/src/test/tbv.cpp +++ b/src/test/tbv.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "tbv.h" static void tst1(unsigned num_bits) { diff --git a/src/test/test_util.h b/src/test/test_util.h index c83a94dbf..c81524b0e 100644 --- a/src/test/test_util.h +++ b/src/test/test_util.h @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #pragma once #include "stopwatch.h" diff --git a/src/test/theory_dl.cpp b/src/test/theory_dl.cpp index 9521a8932..463625c88 100644 --- a/src/test/theory_dl.cpp +++ b/src/test/theory_dl.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "smt_context.h" #include "dl_decl_plugin.h" #include "ast_pp.h" diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp index ee1ec126a..3a229d951 100644 --- a/src/test/theory_pb.cpp +++ b/src/test/theory_pb.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "smt_context.h" #include "ast_pp.h" #include "model_v2_pp.h" diff --git a/src/test/timeout.cpp b/src/test/timeout.cpp index 19daebb12..320006928 100644 --- a/src/test/timeout.cpp +++ b/src/test/timeout.cpp @@ -1,4 +1,10 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + + #include "timeout.h" #include "trace.h" diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 7be048c73..0545ed62c 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include "udoc_relation.h" #include "trace.h" #include "vector.h" diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index e911ff505..7539e7ba3 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -1,3 +1,9 @@ + +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + #include #include #include