Java API: package renaming.

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/api/java/AST.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * The abstract syntax tree (AST) class.

src/api/java/ASTDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 public class ASTDecRefQueue extends IDecRefQueue
 {

src/api/java/ASTMap.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Map from AST to AST

src/api/java/ASTVector.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Vectors of ASTs.

src/api/java/AlgebraicNum.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter) 
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Algebraic numbers

src/api/java/ApplyResult.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * ApplyResult objects represent the result of an application of a tactic to a

src/api/java/ApplyResultDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ApplyResultDecRefQueue extends IDecRefQueue
 {

src/api/java/ArithExpr.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  * **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Arithmetic expressions (int/real)

src/api/java/ArithSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * An arithmetic sort, i.e., Int or Real.

src/api/java/ArrayExpr.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 
 /**

src/api/java/ArraySort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter) 
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Array sorts.

src/api/java/AstMapDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ASTMapDecRefQueue extends IDecRefQueue
 {

src/api/java/AstVectorDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ASTVectorDecRefQueue extends IDecRefQueue
 {

src/api/java/BitVecExpr.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Bit-vector expressions

src/api/java/BitVecNum.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.math.BigInteger;
 

src/api/java/BitVecSort.java

@@ -3,7 +3,7 @@
  * w/ further modifications by:
  * @author Christoph M. Wintersteiger (cwinter)
  **/
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Bit-vector sorts.

src/api/java/BoolExpr.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Boolean expressions

src/api/java/BoolSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A Boolean sort.

src/api/java/Constructor.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Constructors are used for datatype sorts.

src/api/java/ConstructorList.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Lists of constructors

src/api/java/Context.java

@@ -4,10 +4,10 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.util.*;
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * The main interaction with Z3 happens via the Context.

src/api/java/DatatypeExpr.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Datatype expressions

src/api/java/DatatypeSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Datatype sorts.

src/api/java/EnumSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Enumeration sorts.

src/api/java/Expr.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /* using System; */
 

src/api/java/FiniteDomainSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Finite domain sorts.

src/api/java/Fixedpoint.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Object for managing fixedpoints

src/api/java/FixedpointDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class FixedpointDecRefQueue extends IDecRefQueue
 {

src/api/java/FuncDecl.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Function declarations.

src/api/java/FuncInterp.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A function interpretation is represented as a finite map and an 'else' value.

src/api/java/FuncInterpDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class FuncInterpDecRefQueue extends IDecRefQueue
 {

src/api/java/FuncInterpEntryDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class FuncInterpEntryDecRefQueue extends IDecRefQueue
 {

src/api/java/Goal.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * A goal (aka problem). A goal is essentially a set of formulas, that can be

src/api/java/GoalDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class GoalDecRefQueue extends IDecRefQueue
 {

src/api/java/IDecRefQueue.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.util.*;
 

src/api/java/IDisposable.java

@@ -17,7 +17,7 @@ Notes:
     
 --*/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 public class IDisposable
 {

src/api/java/IntExpr.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Int expressions

src/api/java/IntNum.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.math.BigInteger;
 

src/api/java/IntSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * An Integer sort

src/api/java/IntSymbol.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Numbered symbols

src/api/java/ListSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * List sorts.

src/api/java/Log.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Interaction logging for Z3. <remarks> Note that this is a global, static log

src/api/java/Model.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * A Model contains interpretations (assignments) of constants and functions.

src/api/java/ModelDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ModelDecRefQueue extends IDecRefQueue
 {

src/api/java/ParamDescrs.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * A ParamDescrs describes a set of parameters.

src/api/java/ParamDescrsDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ParamDescrsDecRefQueue extends IDecRefQueue
 {

src/api/java/Params.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A ParameterSet represents a configuration in the form of Symbol/value pairs.

src/api/java/ParamsDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ParamsDecRefQueue extends IDecRefQueue
 {

src/api/java/Pattern.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Patterns comprise a list of terms. The list should be non-empty. If the list

src/api/java/Probe.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Probes are used to inspect a goal (aka problem) and collect information that

src/api/java/ProbeDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class ProbeDecRefQueue extends IDecRefQueue
 {

src/api/java/Quantifier.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Quantifier expressions.

src/api/java/RatNum.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.math.BigInteger;
 /**

src/api/java/RealExpr.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Real expressions

src/api/java/RealSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * A real sort

src/api/java/RelationSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Relation sorts.

src/api/java/SetSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Set sorts.

src/api/java/Solver.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Solvers.

src/api/java/SolverDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class SolverDecRefQueue extends IDecRefQueue
 {

src/api/java/Sort.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * The Sort class implements type information for ASTs.

src/api/java/Statistics.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Objects of this class track statistical information about solvers.

src/api/java/StatisticsDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class StatisticsDecRefQueue extends IDecRefQueue
 {

src/api/java/Status.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Status values.

src/api/java/StringSymbol.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Named symbols

src/api/java/Symbol.java

@@ -4,9 +4,9 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
-import com.Microsoft.Z3.Enumerations.*;
+import com.microsoft.z3.enumerations.*;
 
 /**
  * Symbols are used to name several term and type constructors.

src/api/java/Tactic.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Tactics are the basic building block for creating custom solvers for specific

src/api/java/TacticDecRefQueue.java

@@ -3,7 +3,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 class TacticDecRefQueue extends IDecRefQueue
 {

src/api/java/TupleSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Tuple sorts.

src/api/java/UninterpretedSort.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Uninterpreted Sorts

src/api/java/Version.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Version information. <remarks>Note that this class is static.</remarks>

src/api/java/Z3Exception.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 import java.lang.Exception;
 

src/api/java/Z3Object.java

@@ -4,7 +4,7 @@
  * @author Christoph M. Wintersteiger (cwinter)
  **/
 
-package com.Microsoft.Z3;
+package com.microsoft.z3;
 
 /**
  * Internal base class for interfacing with native Z3 objects. Should not be

src/api/java/mk_java.py

@@ -1,11 +1,18 @@
-############################################
+######################################################
 # Copyright (c) 2012 Microsoft Corporation
 # 
 # Auxiliary scripts for generating Java bindings
 # from the managed API.
 #
 # Author: Christoph M. Wintersteiger (cwinter)
-############################################
+######################################################
+
+
+###
+# DO NOT USE THIS SCRIPT! 
+# This script creates a rough draft of a Java API from
+# the managed API, but does not automated the process.
+###
 
 CS="../dotnet/"
 EXT=".cs"