mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	fixing file heads to match z3
This commit is contained in:
		
							parent
							
								
									68fb01c206
								
							
						
					
					
						commit
						e5f5e008aa
					
				
					 14 changed files with 259 additions and 12 deletions
				
			
		| 
						 | 
				
			
			@ -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
 | 
			
		||||
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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 <stdio.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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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 <sstream>
 | 
			
		||||
#include <iostream>
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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"
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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"
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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 <assert.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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
| 
						 | 
				
			
			@ -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
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue