Java API: Added FPA

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

src/api/java/AST.java

@@ -28,7 +28,7 @@ public class AST extends Z3Object
 
     /**
      * Object comparison.
-     * <param name="o">another AST</param>
+     * @param o another AST
      **/    
     public boolean equals(Object o)
     {
@@ -46,7 +46,7 @@ public class AST extends Z3Object
     }
 
     /**
-     * Object Comparison. <param name="other">Another AST</param>
+     * Object Comparison. @param other Another AST
      * 
      * @return Negative if the object should be sorted before <paramref
      *         name="other"/>, positive if after else zero.

src/api/java/ASTMap.java

@@ -39,7 +39,7 @@ class ASTMap extends Z3Object
     /**
      * Finds the value associated with the key <paramref name="k"/>. <remarks>
      * This function signs an error when <paramref name="k"/> is not a key in
-     * the map. </remarks> <param name="k">An AST</param>
+     * the map. </remarks> @param k An AST
      * 
      * @throws Z3Exception
      **/
@@ -51,7 +51,7 @@ class ASTMap extends Z3Object
 
     /**
      * Stores or replaces a new key/value pair in the map. <param name="k">The
-     * key AST</param> <param name="v">The value AST</param>
+     * key AST</param> @param v The value AST
      **/
     public void insert(AST k, AST v) throws Z3Exception
     {

src/api/java/ASTVector.java

@@ -33,7 +33,7 @@ class ASTVector extends Z3Object
     /**
      * Retrieves the i-th object in the vector. <remarks>May throw an
      * IndexOutOfBoundsException when <paramref name="i"/> is out of
-     * range.</remarks> <param name="i">Index</param>
+     * range.</remarks> @param i Index
      * 
      * @return An AST
      * @throws Z3Exception
@@ -62,7 +62,7 @@ class ASTVector extends Z3Object
 
     /**
      * Add the AST <paramref name="a"/> to the back of the vector. The size is
-     * increased by 1. <param name="a">An AST</param>
+     * increased by 1. @param a An AST
      **/
     public void push(AST a) throws Z3Exception
     {

src/api/java/AlgebraicNum.java

@@ -25,7 +25,7 @@ public class AlgebraicNum extends ArithExpr
 	/**
 	 * Return a upper bound for a given real algebraic number. The interval
 	 * isolating the number is smaller than 1/10^<paramref name="precision"/>.
-	 * <seealso cref="Expr.IsAlgebraicNumber"/> <param name="precision">the
+	 * @see Expr.IsAlgebraicNumber <param name="precision">the
 	 * precision of the result</param>
 	 * 
 	 * @return A numeral Expr of sort Real
@@ -33,14 +33,17 @@ public class AlgebraicNum extends ArithExpr
 	public RatNum toUpper(int precision) throws Z3Exception
 	{
 
-		return new RatNum(getContext(), Native.getAlgebraicNumberUpper(getContext()
+		return new RatNum(getContext(), 
-				.nCtx(), getNativeObject(), precision));
+				Native.getAlgebraicNumberUpper(
+						getContext().nCtx(), 
+						getNativeObject(), 
+						precision));
 	}
 
 	/**
 	 * Return a lower bound for the given real algebraic number. The interval
 	 * isolating the number is smaller than 1/10^<paramref name="precision"/>.
-	 * <seealso cref="Expr.IsAlgebraicNumber"/> <param name="precision"></param>
+	 * @see Expr.IsAlgebraicNumber @param precision 
 	 * 
 	 * @return A numeral Expr of sort Real
 	 **/

src/api/java/Expr.java

@@ -40,8 +40,8 @@ public class Expr extends AST
 	/**
 	 * Returns a simplified version of the expression 
 	 * A set of
-	 * parameters <param name="p">a Params object</param> to configure the simplifier 
+	 * parameters @param p a Params object to configure the simplifier 
-	 * <seealso cref="Context.SimplifyHelp"/>
+	 * @see Context.SimplifyHelp
 	 **/
 	public Expr simplify(Params p) throws Z3Exception
 	{
@@ -133,7 +133,7 @@ public class Expr extends AST
 
 	/**
 	 * Substitute every occurrence of <code>from</code> in the expression with
-	 * <code>to</code>. <seealso cref="Substitute(Expr[],Expr[])"/>
+	 * <code>to</code>. @see Substitute(Expr[],Expr[])
 	 **/
 	public Expr substitute(Expr from, Expr to) throws Z3Exception
 	{
@@ -157,7 +157,7 @@ public class Expr extends AST
 
 	/**
 	 * Translates (copies) the term to the Context <paramref name="ctx"/>.
-	 * <param name="ctx">A context</param>
+	 * @param ctx A context
 	 * 
 	 * @return A copy of the term which is associated with <paramref
 	 *         name="ctx"/>
@@ -1682,7 +1682,7 @@ public class Expr extends AST
 	 * Indicates whether the term is a relational clone (copy) <remarks> Create
 	 * a fresh copy (clone) of a relation. The function is logically the
 	 * identity, but in the context of a register machine allows for terms of
-	 * kind <seealso cref="IsRelationUnion"/> to perform destructive updates to
+	 * kind @see IsRelationUnion to perform destructive updates to
 	 * the first argument. </remarks>
 	 **/
 	public boolean isRelationClone() throws Z3Exception

src/api/java/Fixedpoint.java

@@ -163,7 +163,7 @@ public class Fixedpoint extends Z3Object
     }
 
     /**
-     * Creates a backtracking point. <seealso cref="Pop"/>
+     * Creates a backtracking point. @see Pop
      **/
     public void push() throws Z3Exception
     {
@@ -173,7 +173,7 @@ public class Fixedpoint extends Z3Object
     /**
      * Backtrack one backtracking point. <remarks>Note that an exception is
      * thrown if Pop is called without a corresponding <code>Push</code>
-     * </remarks> <seealso cref="Push"/>
+     * </remarks> @see Push
      **/
     public void pop() throws Z3Exception
     {

src/api/java/Global.java

@@ -50,7 +50,7 @@ public final class Global
     /**
      * Get a global (or module) parameter.     
      * <remarks>               
-     * Returns null if the parameter <param name="id">parameter id</param> does not exist.     
+     * Returns null if the parameter @param id parameter id does not exist.     
      * This function cannot be invoked simultaneously from different threads without synchronization.
      * The result string stored in param_value is stored in a shared location.
      * </remarks>
@@ -69,7 +69,7 @@ public final class Global
      * <remarks>
      * This command will not affect already created objects (such as tactics and solvers)
      * </remarks>
-     * <seealso cref="SetParameter"/>
+     * @see SetParameter
      **/
     public static void resetParameters()
     {

src/api/java/InterpolationContext.java

@@ -42,7 +42,7 @@ public class InterpolationContext extends Context
     /** 
      * Constructor.
      *
-     * <remarks><seealso cref="Context.Context(Dictionary&lt;string, string&gt;)"/></remarks>
+     * <remarks>@see Context.Context(Dictionary&lt;string, string&gt;)</remarks>
      **/
     public InterpolationContext(Map<String, String> settings) throws Z3Exception
     { 

src/api/java/Model.java

@@ -26,7 +26,7 @@ public class Model extends Z3Object
 {
     /**
      * Retrieves the interpretation (the assignment) of <paramref name="a"/> in
-     * the model. <param name="a">A Constant</param>
+     * the model. @param a A Constant
      * 
      * @return An expression if the constant has an interpretation in the model,
      *         null otherwise.
@@ -40,7 +40,7 @@ public class Model extends Z3Object
 
     /**
      * Retrieves the interpretation (the assignment) of <paramref name="f"/> in
-     * the model. <param name="f">A function declaration of zero arity</param>
+     * the model. @param f A function declaration of zero arity
      * 
      * @return An expression if the function has an interpretation in the model,
      *         null otherwise.
@@ -242,7 +242,7 @@ public class Model extends Z3Object
      * <remarks> Z3 also provides an intepretation for uninterpreted sorts used
      * in a formula. The interpretation for a sort is a finite set of distinct
      * values. We say this finite set is the "universe" of the sort. </remarks>
-     * <seealso cref="NumSorts"/> <seealso cref="SortUniverse"/>
+     * @see NumSorts"/> <seealso cref="SortUniverse
      * 
      * @throws Z3Exception
      **/
@@ -259,7 +259,7 @@ public class Model extends Z3Object
 
     /**
      * The finite set of distinct values that represent the interpretation for
-     * sort <paramref name="s"/>. <seealso cref="Sorts"/> <param name="s">An
+     * sort <paramref name="s"/>. @see Sorts <param name="s">An
      * uninterpreted sort</param>
      * 
      * @return An array of expressions, where each is an element of the universe

src/api/java/Solver.java

@@ -56,8 +56,8 @@ public class Solver extends Z3Object
     }
 
     /**
-     * The current number of backtracking points (scopes). <seealso cref="Pop"/>
+     * The current number of backtracking points (scopes). @see Pop
-     * <seealso cref="Push"/>
+     * @see Push
      **/
     public int getNumScopes() throws Z3Exception
     {
@@ -66,7 +66,7 @@ public class Solver extends Z3Object
     }
 
     /**
-     * Creates a backtracking point. <seealso cref="Pop"/>
+     * Creates a backtracking point. @see Pop
      **/
     public void push() throws Z3Exception
     {
@@ -84,7 +84,7 @@ public class Solver extends Z3Object
     /**
      * Backtracks <paramref name="n"/> backtracking points. <remarks>Note that
      * an exception is thrown if <paramref name="n"/> is not smaller than
-     * <code>NumScopes</code></remarks> <seealso cref="Push"/>
+     * <code>NumScopes</code></remarks> @see Push
      **/
     public void pop(int n) throws Z3Exception
     {
@@ -193,7 +193,7 @@ public class Solver extends Z3Object
 
     /**
      * Checks whether the assertions in the solver are consistent or not.
-     * <remarks> <seealso cref="Model"/> <seealso cref="UnsatCore"/> <seealso
+     * <remarks> @see Model"/> <seealso cref="UnsatCore <seealso
      * cref="Proof"/> </remarks>
      **/
     public Status check(Expr... assumptions) throws Z3Exception
@@ -219,7 +219,7 @@ public class Solver extends Z3Object
 
     /**
      * Checks whether the assertions in the solver are consistent or not.
-     * <remarks> <seealso cref="Model"/> <seealso cref="UnsatCore"/> <seealso
+     * <remarks> @see Model"/> <seealso cref="UnsatCore <seealso
      * cref="Proof"/> </remarks>
      **/
     public Status check() throws Z3Exception