fixes to Euclidean solver, fixes #100

Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>

src/api/dotnet/ASTMap.cs

@@ -98,11 +98,12 @@ namespace Microsoft.Z3
         /// <summary>
         /// The keys stored in the map.
         /// </summary>
-        public ASTVector Keys
+        public AST[] Keys
         {
             get
             {
-                return new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
+                ASTVector res = new ASTVector(Context, Native.Z3_ast_map_keys(Context.nCtx, NativeObject));
+                return res.ToArray();
             }
         }
 

src/api/dotnet/ASTVector.cs

@@ -99,6 +99,138 @@ namespace Microsoft.Z3
             return Native.Z3_ast_vector_to_string(Context.nCtx, NativeObject);
         }
 
+        /// <summary>
+        /// Translates an AST vector into an AST[]
+        /// </summary>    
+        public AST[] ToArray()
+        {
+            uint n = Size;
+            AST[] res = new AST[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = AST.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into an Expr[]
+        /// </summary>    
+        public Expr[] ToExprArray()
+        {
+            uint n = Size;
+            Expr[] res = new Expr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a BoolExpr[]
+        /// </summary>    
+        public BoolExpr[] ToBoolExprArray()
+        {
+            uint n = Size;
+            BoolExpr[] res = new BoolExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a BitVecExpr[]
+        /// </summary>    
+        public BitVecExpr[] ToBitVecExprArray()
+        {
+            uint n = Size;
+            BitVecExpr[] res = new BitVecExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a ArithExpr[]
+        /// </summary>    
+        public ArithExpr[] ToArithExprArray()
+        {
+            uint n = Size;
+            ArithExpr[] res = new ArithExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a ArrayExpr[]
+        /// </summary>    
+        public ArrayExpr[] ToArrayExprArray()
+        {
+            uint n = Size;
+            ArrayExpr[] res = new ArrayExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a DatatypeExpr[]
+        /// </summary>    
+        public DatatypeExpr[] ToDatatypeExprArray()
+        {
+            uint n = Size;
+            DatatypeExpr[] res = new DatatypeExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a FPExpr[]
+        /// </summary>    
+        public FPExpr[] ToFPExprArray()
+        {
+            uint n = Size;
+            FPExpr[] res = new FPExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a FPRMExpr[]
+        /// </summary>    
+        public FPRMExpr[] ToFPRMExprArray()
+        {
+            uint n = Size;
+            FPRMExpr[] res = new FPRMExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a IntExpr[]
+        /// </summary>    
+        public IntExpr[] ToIntExprArray()
+        {
+            uint n = Size;
+            IntExpr[] res = new IntExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a RealExpr[]
+        /// </summary>    
+        public RealExpr[] ToRealExprArray()
+        {
+            uint n = Size;
+            RealExpr[] res = new RealExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
         #region Internal
         internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }

src/api/dotnet/Fixedpoint.cs

@@ -269,14 +269,6 @@ namespace Microsoft.Z3
                              AST.ArrayLength(queries), AST.ArrayToNative(queries));
         }
 
-        BoolExpr[] ToBoolExprs(ASTVector v) {
-            uint n = v.Size;
-            BoolExpr[] res = new BoolExpr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = new BoolExpr(Context, v[i].NativeObject);
-            return res;
-        }
-
         /// <summary>
         /// Retrieve set of rules added to fixedpoint context.
         /// </summary>                
@@ -286,7 +278,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject)));
+                ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
+                return av.ToBoolExprArray();
             }
         }
 
@@ -299,7 +292,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject)));
+                ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
+                return av.ToBoolExprArray();
             }
         }
 
@@ -321,16 +315,19 @@ namespace Microsoft.Z3
         /// Add the rules to the current fixedpoint context. 
         /// Return the set of queries in the file.
         /// </summary>                
-	public BoolExpr[] ParseFile(string file) {
+        public BoolExpr[] ParseFile(string file)
-            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file)));
+        {
+            ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
+            return av.ToBoolExprArray();
         }
 
         /// <summary>
         /// Similar to ParseFile. Instead it takes as argument a string.
         /// </summary>
-
+        public BoolExpr[] ParseString(string s)
-	public BoolExpr[] ParseString(string s) {
+        {
-            return ToBoolExprs(new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s)));
+            ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
+            return av.ToBoolExprArray();
         }
 
 

src/api/dotnet/InterpolationContext.cs

@@ -47,7 +47,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_get_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+        public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
         {
             Contract.Requires(pf != null);
             Contract.Requires(pat != null);
@@ -59,11 +59,7 @@ namespace Microsoft.Z3
             CheckContextMatch(p);
 
             ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
-            uint n = seq.Size;
+            return seq.ToBoolExprArray();
-            Expr[] res = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = Expr.Create(this, seq[i].NativeObject);
-            return res;
         }
 
         /// <summary> 
@@ -72,7 +68,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_compute_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out ASTVector interp, out Model model)
+        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
         {
             Contract.Requires(pat != null);
             Contract.Requires(p != null);
@@ -84,7 +80,7 @@ namespace Microsoft.Z3
 
             IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
             int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
-            interp = new ASTVector(this, i);
+            interp = new ASTVector(this, i).ToBoolExprArray();
             model = new Model(this, m);
             return (Z3_lbool)r;
         }
@@ -106,7 +102,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_check_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
+        public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
         {
             Contract.Requires(cnsts.Length == parents.Length);
             Contract.Requires(cnsts.Length == interps.Length + 1);

src/api/dotnet/Model.cs

@@ -265,12 +265,8 @@ namespace Microsoft.Z3
             Contract.Requires(s != null);
             Contract.Ensures(Contract.Result<Expr[]>() != null);
 
-            ASTVector nUniv = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));
+            ASTVector av = new ASTVector(Context, Native.Z3_model_get_sort_universe(Context.nCtx, NativeObject, s.NativeObject));            
-            uint n = nUniv.Size;
+            return av.ToExprArray();
-            Expr[] res = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                res[i] = Expr.Create(Context, nUniv[i].NativeObject);
-            return res;
         }
 
         /// <summary>

src/api/dotnet/Solver.cs

@@ -178,8 +178,8 @@ namespace Microsoft.Z3
         {
             get
             {
-                ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
-                return ass.Size;
+                return assertions.Size;
             }
         }
 
@@ -192,12 +192,8 @@ namespace Microsoft.Z3
             {
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
-                ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
+                ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
-                uint n = ass.Size;
+                return assertions.ToBoolExprArray();
-                BoolExpr[] res = new BoolExpr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new BoolExpr(Context, ass[i].NativeObject);
-                return res;
             }
         }
 
@@ -270,18 +266,14 @@ namespace Microsoft.Z3
         /// The result is empty if <c>Check</c> was not invoked before,
         /// if its results was not <c>UNSATISFIABLE</c>, or if core production is disabled.
         /// </remarks>
-        public Expr[] UnsatCore
+        public BoolExpr[] UnsatCore
         {
             get
             {
                 Contract.Ensures(Contract.Result<Expr[]>() != null);
 
                 ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));                
-                uint n = core.Size;
+                return core.ToBoolExprArray();
-                Expr[] res = new Expr[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = Expr.Create(Context, core[i].NativeObject);
-                return res;
             }
         }
 

src/api/java/ASTMap.java

@@ -92,10 +92,10 @@ class ASTMap extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public ASTVector getKeys()
+    public AST[] getKeys()
     {
-        return new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(),
+        ASTVector av = new ASTVector(getContext(), Native.astMapKeys(getContext().nCtx(), getNativeObject()));
-                getNativeObject()));
+        return av.ToArray();
     }
 
     /**

src/api/java/ASTVector.java

@@ -119,4 +119,135 @@ public class ASTVector extends Z3Object
         getContext().getASTVectorDRQ().add(o);
         super.decRef(o);
     }
+    
+    /**
+     * Translates the AST vector into an AST[]
+     * */
+    public AST[] ToArray()
+    {
+        int n = size();
+        AST[] res = new AST[n];
+        for (int i = 0; i < n; i++)
+            res[i] = AST.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+    
+    /**
+     * Translates the AST vector into an Expr[]
+     * */
+    public Expr[] ToExprArray() {
+        int n = size();
+        Expr[] res = new Expr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = Expr.create(getContext(), get(i).getNativeObject());
+        return res;	
+    }
+
+    /**
+     * Translates the AST vector into an BoolExpr[]
+     * */  
+    public BoolExpr[] ToBoolExprArray()
+    {
+        int n = size();
+        BoolExpr[] res = new BoolExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an BitVecExpr[]
+     * */    
+    public BitVecExpr[] ToBitVecExprArray()
+    {
+        int n = size();
+        BitVecExpr[] res = new BitVecExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an ArithExpr[]
+     * */   
+    public ArithExpr[] ToArithExprExprArray()
+    {
+        int n = size();
+        ArithExpr[] res = new ArithExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an ArrayExpr[]
+     * */  
+    public ArrayExpr[] ToArrayExprArray()
+    {
+        int n = size();
+        ArrayExpr[] res = new ArrayExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an DatatypeExpr[]
+     * */ 
+    public DatatypeExpr[] ToDatatypeExprArray()
+    {
+        int n = size();
+        DatatypeExpr[] res = new DatatypeExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an FPExpr[]
+     * */   
+    public FPExpr[] ToFPExprArray()
+    {
+        int n = size();
+        FPExpr[] res = new FPExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an FPRMExpr[]
+     * */
+    public FPRMExpr[] ToFPRMExprArray()
+    {
+        int n = size();
+        FPRMExpr[] res = new FPRMExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an IntExpr[]
+     * */ 
+    public IntExpr[] ToIntExprArray()
+    {
+        int n = size();
+        IntExpr[] res = new IntExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an RealExpr[]
+     * */   
+    public RealExpr[] ToRealExprArray()
+    {
+        int n = size();
+        RealExpr[] res = new RealExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
 }

src/api/java/Fixedpoint.java

@@ -295,14 +295,8 @@ public class Fixedpoint extends Z3Object
      **/
     public BoolExpr[] getRules()
     {
-
+        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
-        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(
+        return v.ToBoolExprArray();
-                getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
     }
 
     /**
@@ -312,14 +306,8 @@ public class Fixedpoint extends Z3Object
      **/
     public BoolExpr[] getAssertions()
     {
-
+        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
-        ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(
+        return v.ToBoolExprArray();
-                getContext().nCtx(), getNativeObject()));
-        int n = v.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), v.get(i).getNativeObject());
-        return res;
     }
 
     /**
@@ -327,12 +315,34 @@ public class Fixedpoint extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Statistics getStatistics() throws Z3Exception
+    public Statistics getStatistics()
     {
         return new Statistics(getContext(), Native.fixedpointGetStatistics(
                 getContext().nCtx(), getNativeObject()));
     }
 
+    /** 
+     * Parse an SMT-LIB2 file with fixedpoint rules. 
+     * Add the rules to the current fixedpoint context. 
+     * Return the set of queries in the file.
+     **/        
+    public BoolExpr[] ParseFile(String file)
+    {
+        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
+        return av.ToBoolExprArray();
+    }
+
+    /** 
+     * Parse an SMT-LIB2 string with fixedpoint rules. 
+     * Add the rules to the current fixedpoint context. 
+     * Return the set of queries in the file.
+     **/ 
+    public BoolExpr[] ParseString(String s)
+    {
+        ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
+        return av.ToBoolExprArray();
+    }
+    
 
     Fixedpoint(Context ctx, long obj) throws Z3Exception
     {

src/api/java/InterpolationContext.java

@@ -73,18 +73,14 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+    public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
     {
         checkContextMatch(pf);
         checkContextMatch(pat);
         checkContextMatch(p);
 
         ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
-        int n = seq.size();
+        return seq.ToBoolExprArray();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(this, seq.get(i).getNativeObject());
-        return res;
     }
 
     public class ComputeInterpolantResult 
@@ -110,13 +106,10 @@ public class InterpolationContext extends Context
         Native.LongPtr n_i = new Native.LongPtr();
         Native.LongPtr n_m = new Native.LongPtr();
         res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
-        if (res.status == Z3_lbool.Z3_L_FALSE) {xx
+        if (res.status == Z3_lbool.Z3_L_FALSE)
-	    res.interp = new BoolExpr[Native.astVectorSize(nCtx(), n_i.value)];
+            res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
-	    for (int i = 0; i < res.interp.Length; ++i) {
+        if (res.status == Z3_lbool.Z3_L_TRUE) 
-		res.interp[i] = new BoolExpr(this, Native.astVectorGet(nCtx(), i));
+            res.model = new Model(this, n_m.value);
-	    }
-	}
-        if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
         return res;
     }
 
@@ -143,7 +136,7 @@ public class InterpolationContext extends Context
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_check_interpolant in the C/C++ API, which is 
     /// well documented.
-    public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
+    public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
     {
         CheckInterpolantResult res = new CheckInterpolantResult();
         Native.StringPtr n_err_str = new Native.StringPtr();

src/api/java/Model.java

@@ -273,11 +273,7 @@ public class Model extends Z3Object
 
         ASTVector nUniv = new ASTVector(getContext(), Native.modelGetSortUniverse(
                 getContext().nCtx(), getNativeObject(), s.getNativeObject()));
-        int n = nUniv.size();
+        return nUniv.ToExprArray();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(getContext(), nUniv.get(i).getNativeObject());
-        return res;
     }
 
     /**

src/api/java/Solver.java

@@ -176,8 +176,7 @@ public class Solver extends Z3Object
      **/
     public int getNumAssertions()
     {
-        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
-                getContext().nCtx(), getNativeObject()));
         return assrts.size();
     }
 
@@ -188,13 +187,8 @@ public class Solver extends Z3Object
      **/
     public BoolExpr[] getAssertions()
     {
-        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(
+        ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
-                getContext().nCtx(), getNativeObject()));
+        return assrts.ToBoolExprArray();
-        int n = assrts.size();
-        BoolExpr[] res = new BoolExpr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = new BoolExpr(getContext(), assrts.get(i).getNativeObject());
-        return res;
     }
 
     /**
@@ -282,16 +276,11 @@ public class Solver extends Z3Object
      * 
      * @throws Z3Exception
      **/
-    public Expr[] getUnsatCore()
+    public BoolExpr[] getUnsatCore()
     {
 
-        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
+        ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
-                getContext().nCtx(), getNativeObject()));
+        return core.ToBoolExprArray();
-        int n = core.size();
-        Expr[] res = new Expr[n];
-        for (int i = 0; i < n; i++)
-            res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
-        return res;
     }
 
     /**

src/api/ml/z3.ml

@@ -192,8 +192,59 @@ struct
 end
 
 
-module AST =
+module rec AST :
-struct    
+sig
+  type ast = z3_native_object
+  val context_of_ast : ast -> context
+  val nc_of_ast : ast -> Z3native.z3_context
+  val ptr_of_ast : ast -> Z3native.ptr
+  val ast_of_ptr : context -> Z3native.ptr -> ast
+  module ASTVector :
+  sig
+    type ast_vector = z3_native_object
+    val create : context -> Z3native.ptr -> ast_vector
+    val mk_ast_vector : context -> ast_vector
+    val get_size : ast_vector -> int
+    val get : ast_vector -> int -> ast
+    val set : ast_vector -> int -> ast -> unit
+    val resize : ast_vector -> int -> unit
+    val push : ast_vector -> ast -> unit
+    val translate : ast_vector -> context -> ast_vector
+    val to_list : ast_vector -> ast list
+    val to_expr_list : ast_vector -> Expr.expr list
+    val to_string : ast_vector -> string
+  end
+  module ASTMap :
+  sig
+    type ast_map = z3_native_object
+    val create : context -> Z3native.ptr -> ast_map
+    val mk_ast_map : context -> ast_map
+    val contains : ast_map -> ast -> bool
+    val find : ast_map -> ast -> ast
+    val insert : ast_map -> ast -> ast -> unit
+    val erase : ast_map -> ast -> unit
+    val reset : ast_map -> unit
+    val get_size : ast_map -> int
+    val get_keys : ast_map -> Expr.expr list
+    val to_string : ast_map -> string
+  end
+  val hash : ast -> int
+  val get_id : ast -> int
+  val get_ast_kind : ast -> Z3enums.ast_kind
+  val is_expr : ast -> bool
+  val is_app : ast -> bool
+  val is_var : ast -> bool
+  val is_quantifier : ast -> bool
+  val is_sort : ast -> bool
+  val is_func_decl : ast -> bool
+  val to_string : ast -> string
+  val to_sexpr : ast -> string
+  val equal : ast -> ast -> bool
+  val compare : ast -> ast -> int
+  val translate : ast -> context -> ast
+  val unwrap_ast : ast -> Z3native.ptr
+  val wrap_ast : context -> Z3native.z3_ast -> ast
+end = struct    
   type ast = z3_native_object
 
   let context_of_ast ( x : ast ) = (z3obj_gc x)
@@ -243,6 +294,16 @@ struct
     let translate ( x : ast_vector ) ( to_ctx : context ) =
       create to_ctx (Z3native.ast_vector_translate (z3obj_gnc x) (z3obj_gno x) (context_gno to_ctx))
 
+    let to_list ( x : ast_vector ) =
+	  let xs = (get_size x) in
+      let f i = (get x i) in
+      mk_list f xs
+
+    let to_expr_list ( x : ast_vector ) =
+	  let xs = (get_size x) in
+      let f i = (Expr.expr_of_ptr (z3obj_gc x) (z3obj_gno (get x i))) in
+      mk_list f xs
+	
     let to_string ( x : ast_vector ) =
       Z3native.ast_vector_to_string (z3obj_gnc x) (z3obj_gno x)
   end
@@ -291,8 +352,7 @@ struct
 	
     let get_keys ( x : ast_map ) =
       let av = ASTVector.create (z3obj_gc x) (Z3native.ast_map_keys (z3obj_gnc x) (z3obj_gno x)) in
-      let f i = (ASTVector.get av i) in
+      (ASTVector.to_expr_list av)
-      mk_list f (ASTVector.get_size av)
 
     let to_string ( x : ast_map ) =
       Z3native.ast_map_to_string (z3obj_gnc x) (z3obj_gno x)
@@ -341,15 +401,27 @@ struct
   let wrap_ast ( ctx : context ) ( ptr : Z3native.ptr ) = ast_of_ptr ctx ptr
 end
 
-open AST
+and Sort :
-
+sig
-
+  type sort = Sort of AST.ast
-module Sort = 
+  val ast_of_sort : Sort.sort -> AST.ast
-struct
+  val sort_of_ptr : context -> Z3native.ptr -> sort
+  val gc : sort -> context
+  val gnc : sort -> Z3native.ptr
+  val gno : sort -> Z3native.ptr
+  val sort_lton : sort list -> Z3native.ptr array
+  val sort_option_lton : sort option list -> Z3native.ptr array
+  val equal : sort -> sort -> bool
+  val get_id : sort -> int
+  val get_sort_kind : sort -> Z3enums.sort_kind
+  val get_name : sort -> Symbol.symbol
+  val to_string : sort -> string
+  val mk_uninterpreted : context -> Symbol.symbol -> sort
+  val mk_uninterpreted_s : context -> string -> sort
+end = struct
   type sort = Sort of AST.ast
 
   let sort_of_ptr : context -> Z3native.ptr -> sort = fun ctx no ->
-    let q = (z3_native_object_of_ast_ptr ctx no) in
     if ((Z3enums.ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no)) != Z3enums.SORT_AST) then
       raise (Z3native.Exception "Invalid coercion")
     else
@@ -364,7 +436,7 @@ struct
         | FINITE_DOMAIN_SORT 
         | RELATION_SORT 
         | FLOATING_POINT_SORT
-	| ROUNDING_MODE_SORT -> Sort(q)
+        | ROUNDING_MODE_SORT -> Sort(z3_native_object_of_ast_ptr ctx no)
         | UNKNOWN_SORT -> raise (Z3native.Exception "Unknown sort kind encountered")
 
   let ast_of_sort s = match s with Sort(x) -> x
@@ -407,10 +479,7 @@ struct
     mk_uninterpreted ctx (Symbol.mk_string ( ctx : context ) s)
 end 
 
-open Sort
+and FuncDecl :
-
-
-module rec FuncDecl :
 sig 
   type func_decl = FuncDecl of AST.ast
   val ast_of_func_decl : FuncDecl.func_decl -> AST.ast
@@ -467,21 +536,21 @@ end = struct
 
   let ast_of_func_decl f = match f with FuncDecl(x) -> x
 
-  let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort list ) ( range : sort )  = 
+  let create_ndr ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort )  = 
     let res = { m_ctx = ctx ;
 		m_n_obj = null ;
 		inc_ref = Z3native.inc_ref ;
 		dec_ref = Z3native.dec_ref } in
-    (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (sort_lton domain) (Sort.gno range))) ;
+    (z3obj_sno res ctx (Z3native.mk_func_decl (context_gno ctx) (Symbol.gno name) (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ;
     (z3obj_create res) ;
     FuncDecl(res)
       
-  let create_pdr ( ctx : context) ( prefix : string ) ( domain : sort list ) ( range : sort ) = 
+  let create_pdr ( ctx : context) ( prefix : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) = 
     let res = { m_ctx = ctx ;
 		m_n_obj = null ;
 		inc_ref = Z3native.inc_ref ;
 		dec_ref = Z3native.dec_ref } in
-    (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (sort_lton domain) (Sort.gno range))) ;
+    (z3obj_sno res ctx (Z3native.mk_fresh_func_decl (context_gno ctx) prefix (List.length domain) (Sort.sort_lton domain) (Sort.gno range))) ;
     (z3obj_create res) ;
     FuncDecl(res)
 
@@ -546,22 +615,22 @@ end = struct
 	| _ -> raise (Z3native.Exception "parameter is not a rational string")
   end
 
-  let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort list ) ( range : sort ) =
+  let mk_func_decl ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort list ) ( range : Sort.sort ) =
     create_ndr ctx name domain range
 
-  let mk_func_decl_s ( ctx : context ) ( name : string ) ( domain : sort list ) ( range : sort ) =
+  let mk_func_decl_s ( ctx : context ) ( name : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) =
     mk_func_decl ctx (Symbol.mk_string ctx name) domain range
 
-  let mk_fresh_func_decl ( ctx : context ) ( prefix : string ) ( domain : sort list ) ( range : sort ) =
+  let mk_fresh_func_decl ( ctx : context ) ( prefix : string ) ( domain : Sort.sort list ) ( range : Sort.sort ) =
     create_pdr ctx prefix domain range
 
-  let mk_const_decl ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) =
+  let mk_const_decl ( ctx : context ) ( name : Symbol.symbol ) ( range : Sort.sort ) =
     create_ndr ctx name [] range
 
-  let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : sort ) =
+  let mk_const_decl_s ( ctx : context ) ( name : string ) ( range : Sort.sort ) =
     create_ndr ctx (Symbol.mk_string ctx name) []  range
 
-  let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : sort ) =
+  let mk_fresh_const_decl ( ctx : context ) ( prefix : string ) ( range : Sort.sort ) =
     create_pdr ctx prefix [] range
 
 
@@ -581,11 +650,11 @@ end = struct
     
   let get_domain ( x : func_decl ) = 
     let n = (get_domain_size x) in
-    let f i = sort_of_ptr (gc x) (Z3native.get_domain (gnc x) (gno x) i) in
+    let f i = Sort.sort_of_ptr (gc x) (Z3native.get_domain (gnc x) (gno x) i) in
     mk_list f n
       
   let get_range ( x : func_decl ) = 
-    sort_of_ptr (gc x) (Z3native.get_range (gnc x) (gno x))
+    Sort.sort_of_ptr (gc x) (Z3native.get_range (gnc x) (gno x))
       
   let get_decl_kind ( x : func_decl ) = (decl_kind_of_int (Z3native.get_decl_kind (gnc x) (gno x)))
 
@@ -599,7 +668,7 @@ end = struct
       | PARAMETER_INT -> Parameter.P_Int (Z3native.get_decl_int_parameter (gnc x) (gno x) i)
       | PARAMETER_DOUBLE -> Parameter.P_Dbl (Z3native.get_decl_double_parameter (gnc x) (gno x) i)
       | PARAMETER_SYMBOL-> Parameter.P_Sym (Symbol.create (gc x) (Z3native.get_decl_symbol_parameter (gnc x) (gno x) i))
-      | PARAMETER_SORT -> Parameter.P_Srt (sort_of_ptr (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i))
+      | PARAMETER_SORT -> Parameter.P_Srt (Sort.sort_of_ptr (gc x) (Z3native.get_decl_sort_parameter (gnc x) (gno x) i))
       | PARAMETER_AST -> Parameter.P_Ast (AST.ast_of_ptr (gc x) (Z3native.get_decl_ast_parameter (gnc x) (gno x) i))
       | PARAMETER_FUNC_DECL -> Parameter.P_Fdl (func_decl_of_ptr (gc x) (Z3native.get_decl_func_decl_parameter (gnc x) (gno x) i))
       | PARAMETER_RATIONAL -> Parameter.P_Rat (Z3native.get_decl_rational_parameter (gnc x) (gno x) i)
@@ -820,29 +889,29 @@ end = struct
     
   let is_well_sorted ( x : expr ) = Z3native.is_well_sorted (gnc x) (gno x)
 
-  let get_sort ( x : expr ) = sort_of_ptr (Expr.gc x) (Z3native.get_sort (gnc x) (gno x))
+  let get_sort ( x : expr ) = Sort.sort_of_ptr (Expr.gc x) (Z3native.get_sort (gnc x) (gno x))
     
   let is_const ( x : expr ) = (match x with Expr(a) -> (AST.is_app a)) &&
     (get_num_args x) == 0 &&
     (FuncDecl.get_domain_size (get_func_decl x)) == 0
     
-  let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : sort ) =
+  let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( range : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_const (context_gno ctx) (Symbol.gno name) (Sort.gno range))
       
-  let mk_const_s ( ctx : context ) ( name : string ) ( range : sort ) =
+  let mk_const_s ( ctx : context ) ( name : string ) ( range : Sort.sort ) =
     mk_const ctx (Symbol.mk_string ctx name) range
 
   let mk_const_f ( ctx : context ) ( f : FuncDecl.func_decl ) = Expr.expr_of_func_app ctx f []
 
-  let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : sort ) =
+  let mk_fresh_const ( ctx : context ) ( prefix : string ) ( range : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_fresh_const (context_gno ctx) prefix (Sort.gno range))
 
   let mk_app ( ctx : context ) ( f : FuncDecl.func_decl ) ( args : expr list ) = expr_of_func_app ctx f args
 
-  let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : sort ) =
+  let mk_numeral_string ( ctx : context ) ( v : string ) ( ty : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno ty))
 
-  let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : sort ) =
+  let mk_numeral_int ( ctx : context ) ( v : int ) ( ty : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno ty))
 
   let equal ( a : expr ) ( b : expr ) = AST.equal (ast_of_expr a) (ast_of_expr b)
@@ -856,7 +925,7 @@ open Expr
 module Boolean = 
 struct      
   let mk_sort ( ctx : context ) =
-    (sort_of_ptr ctx (Z3native.mk_bool_sort (context_gno ctx)))
+    (Sort.sort_of_ptr ctx (Z3native.mk_bool_sort (context_gno ctx)))
 
   let mk_const ( ctx : context ) ( name : Symbol.symbol ) =
     (Expr.mk_const ctx name (mk_sort ctx))
@@ -943,7 +1012,7 @@ struct
     
   module Pattern = 
   struct
-    type pattern = Pattern of ast
+    type pattern = Pattern of AST.ast
 	
     let ast_of_pattern e = match e with Pattern(x) -> x
       
@@ -1002,13 +1071,13 @@ struct
       
   let get_bound_variable_sorts ( x : quantifier ) =
     let n = (get_num_bound x) in
-    let f i = (sort_of_ptr (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) i)) in
+    let f i = (Sort.sort_of_ptr (gc x) (Z3native.get_quantifier_bound_sort (gnc x) (gno x) i)) in
     mk_list f n
       
   let get_body ( x : quantifier ) =
     expr_of_ptr (gc x) (Z3native.get_quantifier_body (gnc x) (gno x))  
 
-  let mk_bound ( ctx : context ) ( index : int ) ( ty : sort ) =
+  let mk_bound ( ctx : context ) ( index : int ) ( ty : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_bound (context_gno ctx) index (Sort.gno ty))
 
   let mk_pattern ( ctx : context ) ( terms : expr list ) =
@@ -1017,14 +1086,14 @@ struct
     else
       Pattern.Pattern(z3_native_object_of_ast_ptr ctx (Z3native.mk_pattern (context_gno ctx) (List.length terms) (expr_lton terms)))
 
-  let mk_forall ( ctx : context ) ( sorts : sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
+  let mk_forall ( ctx : context ) ( sorts : Sort.sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
     if (List.length sorts) != (List.length names) then
       raise (Z3native.Exception "Number of sorts does not match number of names")
     else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
       Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) true 
 				    (match weight with | None -> 1 | Some(x) -> x)
 				    (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns)))
-				    (List.length sorts) (sort_lton sorts)
+				    (List.length sorts) (Sort.sort_lton sorts)
 				    (Symbol.symbol_lton names)
 				    (Expr.gno body)))
     else
@@ -1034,7 +1103,7 @@ struct
 				    (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x))
 				    (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns)))
 				    (List.length nopatterns) (expr_lton nopatterns)
-				    (List.length sorts) (sort_lton sorts)
+				    (List.length sorts) (Sort.sort_lton sorts)
 				    (Symbol.symbol_lton names)
 				    (Expr.gno body)))
 	
@@ -1055,14 +1124,14 @@ struct
 				    (List.length nopatterns) (expr_lton nopatterns)
 				    (Expr.gno body)))
 
-  let mk_exists ( ctx : context ) ( sorts : sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
+  let mk_exists ( ctx : context ) ( sorts : Sort.sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
     if (List.length sorts) != (List.length names) then
       raise (Z3native.Exception "Number of sorts does not match number of names")
     else if ((List.length nopatterns) == 0 && quantifier_id == None && skolem_id == None) then
       Quantifier(expr_of_ptr ctx (Z3native.mk_quantifier (context_gno ctx) false
 				    (match weight with | None -> 1 | Some(x) -> x)
 				    (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns)))
-				    (List.length sorts) (sort_lton sorts)
+				    (List.length sorts) (Sort.sort_lton sorts)
 				    (Symbol.symbol_lton names)
 				    (Expr.gno body)))
     else
@@ -1072,7 +1141,7 @@ struct
 				    (match skolem_id with | None -> null | Some(x) -> (Symbol.gno x))
 				    (List.length patterns) (let f x = (AST.ptr_of_ast (Pattern.ast_of_pattern x)) in (Array.of_list (List.map f patterns)))
 				    (List.length nopatterns) (expr_lton nopatterns)
-				    (List.length sorts) (sort_lton sorts)
+				    (List.length sorts) (Sort.sort_lton sorts)
 				    (Symbol.symbol_lton names)
 				    (Expr.gno body)))
 	
@@ -1093,7 +1162,7 @@ struct
 				    (List.length nopatterns) (expr_lton nopatterns)
 				    (Expr.gno body)))
 
-  let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
+  let mk_quantifier ( ctx : context ) ( universal : bool ) ( sorts : Sort.sort list ) ( names : Symbol.symbol list ) ( body : expr ) ( weight : int option ) ( patterns : Pattern.pattern list ) ( nopatterns : expr list ) ( quantifier_id : Symbol.symbol option ) ( skolem_id : Symbol.symbol option ) =
     if (universal) then
       (mk_forall ctx sorts names body weight patterns nopatterns quantifier_id skolem_id)
     else
@@ -1111,8 +1180,8 @@ end
 
 module Z3Array = 
 struct
-  let mk_sort ( ctx : context ) ( domain : sort ) ( range : sort ) =
+  let mk_sort ( ctx : context ) ( domain : Sort.sort ) ( range : Sort.sort ) =
-    sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range))
+    Sort.sort_of_ptr ctx (Z3native.mk_array_sort (context_gno ctx) (Sort.gno domain) (Sort.gno range))
 
   let is_store ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_STORE)
   let is_select ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SELECT)
@@ -1124,13 +1193,13 @@ struct
     (Z3native.is_app (Expr.gnc x) (Expr.gno x)) &&
       ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == ARRAY_SORT)      
 
-  let get_domain ( x : sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_domain (Sort.gnc x) (Sort.gno x))
+  let get_domain ( x : Sort.sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_domain (Sort.gnc x) (Sort.gno x))
-  let get_range ( x : sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_range (Sort.gnc x) (Sort.gno x))
+  let get_range ( x : Sort.sort ) = Sort.sort_of_ptr (Sort.gc x) (Z3native.get_array_sort_range (Sort.gnc x) (Sort.gno x))
 
-  let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : sort ) ( range : sort ) = 
+  let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( domain : Sort.sort ) ( range : Sort.sort ) = 
     (Expr.mk_const ctx name (mk_sort ctx domain range))
       
-  let mk_const_s ( ctx : context ) ( name : string ) ( domain : sort ) ( range : sort ) =	
+  let mk_const_s ( ctx : context ) ( name : string ) ( domain : Sort.sort ) ( range : Sort.sort ) =	
     mk_const ctx (Symbol.mk_string ctx name) domain range
       
   let mk_select ( ctx : context ) ( a : expr ) ( i : expr ) =
@@ -1139,7 +1208,7 @@ struct
   let mk_store ( ctx : context ) ( a : expr ) ( i : expr ) ( v : expr ) =
     expr_of_ptr ctx (Z3native.mk_store (context_gno ctx) (Expr.gno a) (Expr.gno i) (Expr.gno v))
 
-  let mk_const_array ( ctx : context ) ( domain : sort ) ( v : expr ) =
+  let mk_const_array ( ctx : context ) ( domain : Sort.sort ) ( v : expr ) =
     expr_of_ptr ctx (Z3native.mk_const_array (context_gno ctx) (Sort.gno domain) (Expr.gno v))
 
   let mk_map ( ctx : context ) ( f : func_decl ) ( args : expr list ) =
@@ -1153,8 +1222,8 @@ end
 
 module Set = 
 struct     
-  let mk_sort  ( ctx : context ) ( ty : sort ) =
+  let mk_sort  ( ctx : context ) ( ty : Sort.sort ) =
-    sort_of_ptr ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty))
+    Sort.sort_of_ptr ctx (Z3native.mk_set_sort (context_gno ctx) (Sort.gno ty))
 
   let is_union ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_UNION)
   let is_intersect ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_INTERSECT)
@@ -1163,10 +1232,10 @@ struct
   let is_subset ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_SET_SUBSET)
 
 
-  let mk_empty ( ctx : context ) ( domain : sort ) =
+  let mk_empty ( ctx : context ) ( domain : Sort.sort ) =
     (expr_of_ptr ctx (Z3native.mk_empty_set (context_gno ctx) (Sort.gno domain)))
       
-  let mk_full ( ctx : context ) ( domain : sort ) =
+  let mk_full ( ctx : context ) ( domain : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_full_set (context_gno ctx) (Sort.gno domain))
 
   let mk_set_add  ( ctx : context ) ( set : expr ) ( element : expr ) =
@@ -1199,7 +1268,7 @@ end
 module FiniteDomain = 
 struct  
   let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( size : int ) =
-    (sort_of_ptr ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size))
+    Sort.sort_of_ptr ctx (Z3native.mk_finite_domain_sort (context_gno ctx) (Symbol.gno name) size)
       
   let mk_sort_s ( ctx : context ) ( name : string ) ( size : int ) =
     mk_sort ctx (Symbol.mk_string ctx name) size
@@ -1211,7 +1280,7 @@ struct
 
   let is_lt ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FD_LT)
 
-  let get_size ( x : sort ) = 
+  let get_size ( x : Sort.sort ) = 
     let (r, v) = (Z3native.get_finite_domain_sort_size (Sort.gnc x) (Sort.gno x)) in
     if r then v
     else raise (Z3native.Exception "Conversion failed.")
@@ -1239,11 +1308,11 @@ struct
   let is_select ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_SELECT)
   let is_clone ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_RA_CLONE)
 
-  let get_arity ( x : sort ) = Z3native.get_relation_arity (Sort.gnc x) (Sort.gno x)
+  let get_arity ( x : Sort.sort ) = Z3native.get_relation_arity (Sort.gnc x) (Sort.gno x)
 
-  let get_column_sorts ( x : sort ) = 
+  let get_column_sorts ( x : Sort.sort ) = 
     let n = get_arity x in
-    let f i = (sort_of_ptr (Sort.gc x) (Z3native.get_relation_column (Sort.gnc x) (Sort.gno x) i)) in
+    let f i = (Sort.sort_of_ptr (Sort.gc x) (Z3native.get_relation_column (Sort.gnc x) (Sort.gno x) i)) in
     mk_list f n
 end
   
@@ -1262,7 +1331,7 @@ struct
 
     let _field_nums = FieldNumTable.create 0
 
-    let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
+    let create ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : Sort.sort option list ) ( sort_refs : int list ) =
       let n = (List.length field_names) in
       if n != (List.length sorts) then
 	raise (Z3native.Exception "Number of field names does not match number of sorts")
@@ -1274,7 +1343,7 @@ struct
 		       (Symbol.gno recognizer) 
 		       n
 		       (Symbol.symbol_lton field_names)
-		       (sort_option_lton sorts)
+		       (Sort.sort_option_lton sorts)
 		       (Array.of_list sort_refs)) in
 	  let no : constructor = { m_ctx = ctx ;
 				   m_n_obj = null ;
@@ -1321,17 +1390,17 @@ struct
       res       
   end
     
-  let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
+  let mk_constructor ( ctx : context ) ( name : Symbol.symbol ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : Sort.sort option list ) ( sort_refs : int list ) =
     Constructor.create ctx name recognizer field_names sorts sort_refs
 
 
-  let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : sort option list ) ( sort_refs : int list ) =
+  let mk_constructor_s ( ctx : context ) ( name : string ) ( recognizer : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( sorts : Sort.sort option list ) ( sort_refs : int list ) =
     mk_constructor ctx (Symbol.mk_string ctx name) recognizer field_names sorts sort_refs
 
   let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( constructors : Constructor.constructor list ) =
     let f x = (z3obj_gno x) in 
     let (x,_) = (Z3native.mk_datatype (context_gno ctx) (Symbol.gno name) (List.length constructors) (Array.of_list (List.map f constructors))) in
-    sort_of_ptr ctx x
+    Sort.sort_of_ptr ctx x
 
   let mk_sort_s ( ctx : context ) ( name : string ) ( constructors : Constructor.constructor list ) =
     mk_sort ctx (Symbol.mk_string ctx name) constructors
@@ -1341,7 +1410,7 @@ struct
     let f e = (AST.ptr_of_ast (ConstructorList.create ctx e)) in
     let cla = (Array.of_list (List.map f c)) in
     let (r, a) = (Z3native.mk_datatypes (context_gno ctx) n (Symbol.symbol_lton names) cla) in
-    let g i = (sort_of_ptr ctx (Array.get r i)) in
+    let g i = (Sort.sort_of_ptr ctx (Array.get r i)) in
     mk_list g (Array.length r)
 
   let mk_sorts_s ( ctx : context ) ( names : string list ) ( c : Constructor.constructor list list ) =
@@ -1352,19 +1421,19 @@ struct
       )
       c
 
-  let get_num_constructors ( x : sort ) = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)
+  let get_num_constructors ( x : Sort.sort ) = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)
 
-  let get_constructors ( x : sort ) = 
+  let get_constructors ( x : Sort.sort ) = 
     let n = (get_num_constructors x) in
     let f i = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) i) in
     mk_list f n
 
-  let get_recognizers ( x : sort ) = 
+  let get_recognizers ( x : Sort.sort ) = 
     let n = (get_num_constructors x) in
     let f i = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i) in
     mk_list f n
       
-  let get_accessors ( x : sort ) =
+  let get_accessors ( x : Sort.sort ) =
     let n = (get_num_constructors x) in
     let f i = (
       let fd = func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) i) in
@@ -1380,80 +1449,80 @@ module Enumeration =
 struct 
   let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( enum_names : Symbol.symbol list ) =
     let (a, _, _) = (Z3native.mk_enumeration_sort (context_gno ctx) (Symbol.gno name) (List.length enum_names) (Symbol.symbol_lton enum_names)) in
-    sort_of_ptr ctx a
+    Sort.sort_of_ptr ctx a
 
   let mk_sort_s ( ctx : context ) ( name : string ) ( enum_names : string list ) =
     mk_sort ctx (Symbol.mk_string ctx name) (Symbol.mk_strings ctx enum_names)
 
-  let get_const_decls ( x : sort ) =
+  let get_const_decls ( x : Sort.sort ) =
     let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)  in
     let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x)  i)) in
     mk_list f n
 
-  let get_const_decl ( x : sort ) ( inx : int ) =
+  let get_const_decl ( x : Sort.sort ) ( inx : int ) =
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x) inx)
 
-  let get_consts ( x : sort ) =
+  let get_consts ( x : Sort.sort ) =
     let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)  in
     let f i = (Expr.mk_const_f (Sort.gc x) (get_const_decl x i)) in
     mk_list f n
 
-  let get_const ( x : sort ) ( inx : int ) =
+  let get_const ( x : Sort.sort ) ( inx : int ) =
     Expr.mk_const_f (Sort.gc x) (get_const_decl x inx)
 
-  let get_tester_decls ( x : sort ) = 
+  let get_tester_decls ( x : Sort.sort ) = 
     let n = Z3native.get_datatype_sort_num_constructors (Sort.gnc x) (Sort.gno x)  in
     let f i = (func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) i)) in
     mk_list f n
       
-  let get_tester_decl ( x : sort ) ( inx : int ) = 
+  let get_tester_decl ( x : Sort.sort ) ( inx : int ) = 
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x) inx)
 end
 
 
 module Z3List = 
 struct     
-  let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : sort ) =
+  let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( elem_sort : Sort.sort ) =
     let (r, _, _, _, _, _, _) = (Z3native.mk_list_sort (context_gno ctx) (Symbol.gno name) (Sort.gno elem_sort)) in
-    sort_of_ptr ctx r 
+    Sort.sort_of_ptr ctx r 
       
-  let mk_list_s ( ctx : context ) (name : string) elem_sort =
+  let mk_list_s ( ctx : context ) ( name : string ) elem_sort =
     mk_sort ctx (Symbol.mk_string ctx name) elem_sort
 
-  let get_nil_decl ( x : sort ) = 
+  let get_nil_decl ( x : Sort.sort ) = 
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x)  0)
 
-  let get_is_nil_decl ( x : sort ) = 
+  let get_is_nil_decl ( x : Sort.sort ) = 
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x)  0)
 
-  let get_cons_decl ( x : sort ) = 
+  let get_cons_decl ( x : Sort.sort ) = 
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor (Sort.gnc x) (Sort.gno x)  1)
 
-  let get_is_cons_decl ( x : sort ) =
+  let get_is_cons_decl ( x : Sort.sort ) =
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_recognizer (Sort.gnc x) (Sort.gno x)  1)
 
-  let get_head_decl ( x : sort )  = 
+  let get_head_decl ( x : Sort.sort )  = 
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor_accessor (Sort.gnc x) (Sort.gno x) 1 0)
 
-  let get_tail_decl ( x : sort ) =
+  let get_tail_decl ( x : Sort.sort ) =
     func_decl_of_ptr (Sort.gc x) (Z3native.get_datatype_sort_constructor_accessor (Sort.gnc x) (Sort.gno x) 1 1)
 
-  let nil ( x : sort ) = expr_of_func_app (Sort.gc x) (get_nil_decl x) []
+  let nil ( x : Sort.sort ) = expr_of_func_app (Sort.gc x) (get_nil_decl x) []
 end
 
 
 module Tuple = 
 struct
-  let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( field_sorts : sort list ) =
+  let mk_sort ( ctx : context ) ( name : Symbol.symbol ) ( field_names : Symbol.symbol list ) ( field_sorts : Sort.sort list ) =
-    let (r, _, _) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (List.length field_names) (Symbol.symbol_lton field_names) (sort_lton field_sorts)) in 
+    let (r, _, _) = (Z3native.mk_tuple_sort (context_gno ctx) (Symbol.gno name) (List.length field_names) (Symbol.symbol_lton field_names) (Sort.sort_lton field_sorts)) in 
-    sort_of_ptr ctx r
+    Sort.sort_of_ptr ctx r
 
-  let get_mk_decl ( x : sort ) =
+  let get_mk_decl ( x : Sort.sort ) =
     func_decl_of_ptr (Sort.gc x) (Z3native.get_tuple_sort_mk_decl (Sort.gnc x) (Sort.gno x))
 
-  let get_num_fields ( x : sort ) = Z3native.get_tuple_sort_num_fields (Sort.gnc x) (Sort.gno x)
+  let get_num_fields ( x : Sort.sort ) = Z3native.get_tuple_sort_num_fields (Sort.gnc x) (Sort.gno x)
     
-  let get_field_decls ( x : sort ) = 
+  let get_field_decls ( x : Sort.sort ) = 
     let n = get_num_fields x in
     let f i = func_decl_of_ptr (Sort.gc x) (Z3native.get_tuple_sort_field_decl (Sort.gnc x) (Sort.gno x) i) in
     mk_list f n
@@ -1510,7 +1579,7 @@ struct
   module Integer =
   struct     
     let mk_sort ( ctx : context ) =
-      sort_of_ptr ctx (Z3native.mk_int_sort (context_gno ctx))
+      Sort.sort_of_ptr ctx (Z3native.mk_int_sort (context_gno ctx))
 
     let get_int ( x : expr ) = 
       let (r, v) = Z3native.get_numeral_int (Expr.gnc x) (Expr.gno x) in
@@ -1553,7 +1622,7 @@ struct
   module Real =
   struct  
     let mk_sort ( ctx : context ) =
-      sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx))	
+      Sort.sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx))	
 
     let get_numerator ( x : expr ) =
       expr_of_ptr (Expr.gc x) (Z3native.get_numerator (Expr.gnc x) (Expr.gno x))
@@ -1649,7 +1718,7 @@ end
 module BitVector =
 struct  
   let mk_sort ( ctx : context ) size =
-    sort_of_ptr ctx (Z3native.mk_bv_sort (context_gno ctx) size)
+    Sort.sort_of_ptr ctx (Z3native.mk_bv_sort (context_gno ctx) size)
   let is_bv ( x : expr ) =
     ((sort_kind_of_int (Z3native.get_sort_kind (Expr.gnc x) (Z3native.get_sort (Expr.gnc x) (Expr.gno x)))) == BV_SORT)
   let is_bv_numeral ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BNUM)
@@ -1703,7 +1772,7 @@ struct
   let is_bv2int ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_BV2INT)
   let is_bv_carry ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_CARRY)
   let is_bv_xor3 ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_XOR3)
-  let get_size (x : sort ) = Z3native.get_bv_sort_size (Sort.gnc x) (Sort.gno x)
+  let get_size (x : Sort.sort ) = Z3native.get_bv_sort_size (Sort.gnc x) (Sort.gno x)
   let get_int ( x : expr ) = 
     let (r, v) = Z3native.get_numeral_int (Expr.gnc x) (Expr.gno x) in
     if r then v
@@ -1817,7 +1886,7 @@ struct
   module RoundingMode = 
   struct
 	let mk_sort ( ctx : context ) =
-	  (sort_of_ptr ctx (Z3native.mk_fpa_rounding_mode_sort (context_gno ctx)))
+	  (Sort.sort_of_ptr ctx (Z3native.mk_fpa_rounding_mode_sort (context_gno ctx)))
 	let is_fprm ( x : expr ) =
 	  (Sort.get_sort_kind (Expr.get_sort(x))) == ROUNDING_MODE_SORT
 	let mk_round_nearest_ties_to_even ( ctx : context ) = 
@@ -1843,40 +1912,40 @@ struct
   end
 	
   let mk_sort ( ctx : context ) ( ebits : int ) ( sbits : int ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort (context_gno ctx) ebits sbits))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort (context_gno ctx) ebits sbits))
   let mk_sort_half ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_half (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_half (context_gno ctx)))
   let mk_sort_16 ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_16 (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_16 (context_gno ctx)))
   let mk_sort_single ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_single (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_single (context_gno ctx)))
   let mk_sort_32 ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_32 (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_32 (context_gno ctx)))
   let mk_sort_double ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_double (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_double (context_gno ctx)))
   let mk_sort_64 ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_64 (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_64 (context_gno ctx)))
   let mk_sort_quadruple ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_quadruple (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_quadruple (context_gno ctx)))
   let mk_sort_128 ( ctx : context ) =
-	(sort_of_ptr ctx (Z3native.mk_fpa_sort_128 (context_gno ctx)))
+	(Sort.sort_of_ptr ctx (Z3native.mk_fpa_sort_128 (context_gno ctx)))
 
-  let mk_nan ( ctx : context ) ( s : sort ) =
+  let mk_nan ( ctx : context ) ( s : Sort.sort ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_nan (context_gno ctx) (Sort.gno s)))
-  let mk_inf ( ctx : context ) ( s : sort ) ( negative : bool ) =
+  let mk_inf ( ctx : context ) ( s : Sort.sort ) ( negative : bool ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_inf (context_gno ctx) (Sort.gno s) negative))
-  let mk_zero ( ctx : context ) ( s : sort ) ( negative : bool ) =
+  let mk_zero ( ctx : context ) ( s : Sort.sort ) ( negative : bool ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative))
 
   let mk_fp ( ctx : context ) ( sign : expr ) ( exponent : expr ) ( significand : expr ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand)))
-  let mk_numeral_f ( ctx : context ) ( value : float ) ( s : sort ) =
+  let mk_numeral_f ( ctx : context ) ( value : float ) ( s : Sort.sort ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s)))
-  let mk_numeral_i ( ctx : context ) ( value : int ) ( s : sort ) =
+  let mk_numeral_i ( ctx : context ) ( value : int ) ( s : Sort.sort ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_numeral_int (context_gno ctx) value (Sort.gno s)))
-  let mk_numeral_i_u ( ctx : context ) ( sign : bool ) ( exponent : int ) ( significand : int ) ( s : sort ) =
+  let mk_numeral_i_u ( ctx : context ) ( sign : bool ) ( exponent : int ) ( significand : int ) ( s : Sort.sort ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_numeral_int64_uint64 (context_gno ctx) sign exponent significand (Sort.gno s)))
-  let mk_numeral_s ( ctx : context ) ( v : string ) ( s : sort ) =
+  let mk_numeral_s ( ctx : context ) ( v : string ) ( s : Sort.sort ) =
     (expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno s)))
 
   let is_fp ( x : expr ) = (Sort.get_sort_kind (Expr.get_sort x)) == FLOATING_POINT_SORT
@@ -1912,9 +1981,9 @@ struct
   let is_to_ieee_bv ( x : expr ) = (AST.is_app (Expr.ast_of_expr x)) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) == OP_FPA_TO_IEEE_BV)
 	
   let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
-  let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( s : sort ) =
+  let mk_const ( ctx : context ) ( name : Symbol.symbol ) ( s : Sort.sort ) =
     Expr.mk_const ctx name s
-  let mk_const_s ( ctx : context ) ( name : string ) ( s : sort ) =
+  let mk_const_s ( ctx : context ) ( name : string ) ( s : Sort.sort ) =
     mk_const ctx (Symbol.mk_string ctx name) s
 
   let mk_abs ( ctx : context ) ( t : expr ) =
@@ -1965,15 +2034,15 @@ struct
     expr_of_ptr ctx (Z3native.mk_fpa_is_negative (context_gno ctx) (Expr.gno t))
   let mk_is_positive ( ctx : context ) ( t : expr ) =
     expr_of_ptr ctx (Z3native.mk_fpa_is_positive (context_gno ctx) (Expr.gno t))
-  let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : sort ) =
+  let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_fp_bv (context_gno ctx) (Expr.gno t) (Sort.gno s))
-  let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) =
+  let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_fp_float (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
-  let mk_to_fp_real ( ctx : context ) ( rm : expr ) ( t : expr ) ( s : sort ) =
+  let mk_to_fp_real ( ctx : context ) ( rm : expr ) ( t : expr ) ( s : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_fp_real (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
-  let mk_to_fp_signed  ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) =
+  let mk_to_fp_signed  ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_fp_signed (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
-  let mk_to_fp_unsigned  ( ctx : context ) ( rm : expr) ( t : expr ) ( s : sort ) =
+  let mk_to_fp_unsigned  ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_fp_unsigned (context_gno ctx) (Expr.gno rm) (Expr.gno t) (Sort.gno s))
   let mk_to_ubv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_ubv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size)
@@ -1982,9 +2051,9 @@ struct
   let mk_to_real ( ctx : context ) ( t : expr ) =
     expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t))
 
-  let get_ebits ( ctx : context ) ( s : sort ) =
+  let get_ebits ( ctx : context ) ( s : Sort.sort ) =
 	(Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s))
-  let get_sbits ( ctx : context ) ( s : sort ) =
+  let get_sbits ( ctx : context ) ( s : Sort.sort ) =
 	(Z3native.fpa_get_sbits (context_gno ctx) (Sort.gno s))
   let get_numeral_sign ( ctx : context ) ( t : expr ) =
 	(Z3native.fpa_get_numeral_sign (context_gno ctx) (Expr.gno t))
@@ -1997,7 +2066,7 @@ struct
 
   let mk_to_ieee_bv ( ctx : context ) ( t : expr ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_to_ieee_bv (context_gno ctx) (Expr.gno t)))
-  let mk_to_fp_int_real ( ctx : context ) ( rm : expr ) ( exponent : expr ) ( significand : expr ) ( s : sort ) =
+  let mk_to_fp_int_real ( ctx : context ) ( rm : expr ) ( exponent : expr ) ( significand : expr ) ( s : Sort.sort ) =
 	(expr_of_ptr ctx (Z3native.mk_fpa_to_fp_int_real (context_gno ctx) (Expr.gno rm) (Expr.gno exponent) (Expr.gno significand) (Sort.gno s)))
 
   let numeral_to_string ( x : expr ) = Z3native.get_numeral_string (Expr.gnc x) (Expr.gno x)
@@ -2280,14 +2349,12 @@ struct
     
   let get_sorts ( x : model ) =
     let n = (get_num_sorts x) in
-    let f i = (sort_of_ptr (z3obj_gc x) (Z3native.model_get_sort (z3obj_gnc x) (z3obj_gno x) i)) in
+    let f i = (Sort.sort_of_ptr (z3obj_gc x) (Z3native.model_get_sort (z3obj_gnc x) (z3obj_gno x) i)) in
     mk_list f n
 
-  let sort_universe ( x : model ) ( s : sort ) =
+  let sort_universe ( x : model ) ( s : Sort.sort ) =
-    let n_univ = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in
+    let av = AST.ASTVector.create (z3obj_gc x) (Z3native.model_get_sort_universe (z3obj_gnc x) (z3obj_gno x) (Sort.gno s)) in
-    let n = (AST.ASTVector.get_size n_univ) in
+    (AST.ASTVector.to_expr_list av)
-    let f i = (AST.ASTVector.get n_univ i) in
-    mk_list f n
 
   let to_string ( x : model ) = Z3native.model_to_string (z3obj_gnc x) (z3obj_gno x) 
 end
@@ -2475,27 +2542,8 @@ struct
 end
 
 
-module Solver =
+module Statistics =
 struct	
-  type solver = z3_native_object
-  type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
-
-  let create ( ctx : context ) ( no : Z3native.ptr ) = 
-    let res : solver = { m_ctx = ctx ;
-			 m_n_obj = null ;
-			 inc_ref = Z3native.solver_inc_ref ;
-			 dec_ref = Z3native.solver_dec_ref } in
-    (z3obj_sno res ctx no) ;
-    (z3obj_create res) ;
-    res
-      
-  let string_of_status ( s : status) = match s with
-    | UNSATISFIABLE -> "unsatisfiable"
-    | SATISFIABLE -> "satisfiable" 
-    | _ -> "unknown"
-
-  module Statistics =
-  struct	
   type statistics = z3_native_object
 
   let create ( ctx : context ) ( no : Z3native.ptr ) = 
@@ -2576,7 +2624,27 @@ struct
   let get ( x : statistics ) ( key : string ) =
     let f p c = (if ((Entry.get_key c) == key) then (Some c) else p) in
     List.fold_left f None (get_entries x)
-  end
+end
+
+
+module Solver =
+struct      
+  type solver = z3_native_object
+  type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
+
+  let create ( ctx : context ) ( no : Z3native.ptr ) = 
+    let res : solver = { m_ctx = ctx ;
+			 m_n_obj = null ;
+			 inc_ref = Z3native.solver_inc_ref ;
+			 dec_ref = Z3native.solver_dec_ref } in
+    (z3obj_sno res ctx no) ;
+    (z3obj_create res) ;
+    res
+      
+  let string_of_status ( s : status) = match s with
+    | UNSATISFIABLE -> "unsatisfiable"
+    | SATISFIABLE -> "satisfiable" 
+    | _ -> "unknown"
 
   let get_help ( x : solver ) = Z3native.solver_get_help (z3obj_gnc x) (z3obj_gno x)
 
@@ -2613,10 +2681,8 @@ struct
     (AST.ASTVector.get_size a)
 
   let get_assertions ( x : solver ) =
-    let a = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in
+    let av = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_assertions (z3obj_gnc x) (z3obj_gno x)) in
-    let n = (AST.ASTVector.get_size a) in
+    (AST.ASTVector.to_expr_list av)
-    let f i = (expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get a i))) in
-    mk_list f n
 
   let check ( x : solver ) ( assumptions : expr list ) =
     let r = 
@@ -2646,10 +2712,8 @@ struct
       Some (expr_of_ptr (z3obj_gc x) q)
 	
   let get_unsat_core ( x : solver ) =
-    let cn = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in 
+    let av = AST.ASTVector.create (z3obj_gc x) (Z3native.solver_get_unsat_core (z3obj_gnc x) (z3obj_gno x)) in 
-    let n = (AST.ASTVector.get_size cn) in
+    (AST.ASTVector.to_expr_list av)
-    let f i = (AST.ASTVector.get cn i) in
-    mk_list f n
 
   let get_reason_unknown ( x : solver ) =  Z3native.solver_get_reason_unknown (z3obj_gnc x) (z3obj_gno x)
 
@@ -2720,7 +2784,7 @@ struct
       | _ -> Solver.UNKNOWN
 
   let query_r ( x : fixedpoint ) ( relations : func_decl list ) =
-    let f x = ptr_of_ast (ast_of_func_decl x) in
+    let f x = AST.ptr_of_ast (ast_of_func_decl x) in
     match (lbool_of_int (Z3native.fixedpoint_query_relations (z3obj_gnc x) (z3obj_gno x) (List.length relations) (Array.of_list (List.map f relations)))) with
       | L_TRUE -> Solver.SATISFIABLE
       | L_FALSE -> Solver.UNSATISFIABLE
@@ -2768,18 +2832,26 @@ struct
     Z3native.fixedpoint_to_string (z3obj_gnc x) (z3obj_gno x) (List.length queries) (Array.of_list (List.map f queries))
 
   let get_rules ( x : fixedpoint ) = 
-    let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in
+    let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_rules (z3obj_gnc x) (z3obj_gno x))) in
-    let n = (AST.ASTVector.get_size v) in
+    (AST.ASTVector.to_expr_list av)
-    let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in
-    mk_list f n
 
   let get_assertions ( x : fixedpoint ) = 
-    let v = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in
+    let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_get_assertions (z3obj_gnc x) (z3obj_gno x))) in
-    let n = (AST.ASTVector.get_size v) in
+    (AST.ASTVector.to_expr_list av)
-    let f i =(expr_of_ptr (z3obj_gc x) (z3obj_gno (AST.ASTVector.get v i))) in
-    mk_list f n
 
   let mk_fixedpoint ( ctx : context ) = create ctx
+
+  let get_statistics ( x : fixedpoint ) =
+    let s = Z3native.fixedpoint_get_statistics (z3obj_gnc x) (z3obj_gno x) in
+    (Statistics.create (z3obj_gc x) s)
+
+  let parse_string ( x : fixedpoint ) ( s : string ) =
+    let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_from_string (z3obj_gnc x) (z3obj_gno x) s)) in
+    (AST.ASTVector.to_expr_list av)
+
+  let parse_file ( x : fixedpoint ) ( filename : string ) =
+    let av = (AST.ASTVector.create (z3obj_gc x) (Z3native.fixedpoint_from_file (z3obj_gnc x) (z3obj_gno x) filename)) in
+    (AST.ASTVector.to_expr_list av)
 end
 
 
@@ -2790,7 +2862,7 @@ struct
       (List.length assumptions) (let f x = Expr.gno (x) in (Array.of_list (List.map f assumptions)))
       (Expr.gno formula)
 
-  let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
+  let parse_smtlib_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
     let csn = (List.length sort_names) in
     let cs = (List.length sorts) in
     let cdn = (List.length decl_names) in
@@ -2801,12 +2873,12 @@ struct
       Z3native.parse_smtlib_string (context_gno ctx) str 
 	    cs 
 	    (Symbol.symbol_lton sort_names)
-	(sort_lton sorts)
+	    (Sort.sort_lton sorts)
 	    cd 
 	    (Symbol.symbol_lton decl_names)
 	    (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls)))
 	
-  let parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
+  let parse_smtlib_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
     let csn = (List.length sort_names) in
     let cs = (List.length sorts) in
     let cdn = (List.length decl_names) in
@@ -2817,7 +2889,7 @@ struct
       Z3native.parse_smtlib_file (context_gno ctx) file_name
 	    cs 
 	    (Symbol.symbol_lton sort_names)
-	(sort_lton sorts)
+	    (Sort.sort_lton sorts)
 	    cd 
 	    (Symbol.symbol_lton decl_names)
 	    (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls)))
@@ -2847,10 +2919,10 @@ struct
     
   let get_smtlib_sorts ( ctx : context ) = 
     let n = (get_num_smtlib_sorts ctx) in
-    let f i = (sort_of_ptr ctx (Z3native.get_smtlib_sort (context_gno ctx) i)) in
+    let f i = (Sort.sort_of_ptr ctx (Z3native.get_smtlib_sort (context_gno ctx) i)) in
     mk_list f n
 
-  let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
+  let parse_smtlib2_string ( ctx : context ) ( str : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
     let csn = (List.length sort_names) in
     let cs = (List.length sorts) in
     let cdn = (List.length decl_names) in
@@ -2861,12 +2933,12 @@ struct
       (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) str 
 			              cs 
 			              (Symbol.symbol_lton sort_names)
-			  (sort_lton sorts)
+			              (Sort.sort_lton sorts)
 			              cd 
 			              (Symbol.symbol_lton decl_names)
 			              (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls)))))
 	    
-  let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
+  let parse_smtlib2_file ( ctx : context ) ( file_name : string ) ( sort_names : Symbol.symbol list ) ( sorts : Sort.sort list ) ( decl_names : Symbol.symbol list ) ( decls : func_decl list ) =
     let csn = (List.length sort_names) in
     let cs = (List.length sorts) in
     let cdn = (List.length decl_names) in
@@ -2877,7 +2949,7 @@ struct
       (expr_of_ptr ctx (Z3native.parse_smtlib2_string (context_gno ctx) file_name
 			              cs 
 			              (Symbol.symbol_lton sort_names)
-			  (sort_lton sorts)
+			              (Sort.sort_lton sorts)
 			              cd 
 			              (Symbol.symbol_lton decl_names)
 			              (let f x = FuncDecl.gno x in (Array.of_list (List.map f decls)))))
@@ -2902,13 +2974,16 @@ struct
     res
 
   let get_interpolant ( ctx : context ) ( pf : expr ) ( pat: expr ) ( p : Params.params ) =
-    (ASTVector.create ctx (Z3native.get_interpolant (context_gno ctx) (Expr.gno pf) (Expr.gno pat) (z3obj_gno p)))
+    let av = (AST.ASTVector.create ctx (Z3native.get_interpolant (context_gno ctx) (Expr.gno pf) (Expr.gno pat) (z3obj_gno p))) in
+    AST.ASTVector.to_expr_list av
       
   let compute_interpolant ( ctx : context ) ( pat : expr ) ( p : Params.params ) =
     let (r, interp, model) = (Z3native.compute_interpolant (context_gno ctx) (Expr.gno pat) (z3obj_gno p)) in
-    match (lbool_of_int r) with
+    let res = (lbool_of_int r) in
-      | L_TRUE -> ((ASTVector.create ctx interp), (Model.create ctx model))
+    match res with
-      | _ -> raise (Z3native.Exception "Error computing interpolant.")
+      | L_TRUE -> (res, None, Some(Model.create ctx model))
+      | L_FALSE -> (res, Some((AST.ASTVector.to_expr_list (AST.ASTVector.create ctx interp))), None)
+      | _ -> (res, None, None)
        
   let get_interpolation_profile ( ctx : context ) =
     (Z3native.interpolation_profile (context_gno ctx))

src/api/ml/z3.mli

@@ -123,7 +123,7 @@ sig
 end
 
 (** The abstract syntax tree (AST) module *)
-module AST :
+module rec AST :
 sig
   type ast 
 
@@ -156,6 +156,12 @@ sig
 		@return A new ASTVector *)
     val translate : ast_vector -> context -> ast_vector
 
+    (** Translates the ASTVector into an (Ast.ast list) *)
+    val to_list : ast_vector -> ast list
+
+    (** Translates the ASTVector into an (Expr.expr list) *)
+    val to_expr_list : ast_vector -> Expr.expr list
+
     (** Retrieves a string representation of the vector. *)
     val to_string : ast_vector -> string
   end
@@ -189,7 +195,7 @@ sig
     val get_size : ast_map -> int
 
     (** The keys stored in the map. *)
-    val get_keys : ast_map -> ast list
+    val get_keys : ast_map -> Expr.expr list
 
     (** Retrieves a string representation of the map.*)
     val to_string : ast_map -> string
@@ -260,7 +266,7 @@ sig
 end
 
 (** The Sort module implements type information for ASTs *)
-module Sort :
+and Sort :
 sig
   type sort = Sort of AST.ast
 
@@ -291,7 +297,7 @@ sig
 end
 
 (** Function declarations *)
-module rec FuncDecl :
+and FuncDecl :
 sig
   type func_decl = FuncDecl of AST.ast
 
@@ -2751,7 +2757,7 @@ sig
   (** The finite set of distinct values that represent the interpretation of a sort. 
       {!get_sorts}
       @return A list of expressions, where each is an element of the universe of the sort *)
-  val sort_universe : model -> Sort.sort -> AST.ast list
+  val sort_universe : model -> Sort.sort -> Expr.expr list
     
   (** Conversion of models to strings. 
       @return A string representation of the model. *)
@@ -2938,22 +2944,13 @@ sig
   val interrupt : context -> unit
 end
 
-(** Solvers *)
+(** Objects that track statistical information. *)
-module Solver :
+module Statistics :
 sig
-  type solver 
-  type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
-      
-  val string_of_status : status -> string
-
-  (** Objects that track statistical information about solvers. *)
-  module Statistics :
-  sig
   type statistics 
 	
   (** Statistical data is organized into pairs of \[Key, Entry\], where every
-		  Entry is either a floating point or integer value.
+	  Entry is either a floating point or integer value. *)
-    *)
   module Entry :
   sig
     type statistics_entry
@@ -2994,7 +2991,15 @@ sig
 
   (** The value of a particular statistical counter. *)        
   val get : statistics -> string -> Entry.statistics_entry option
-  end
+end
+
+(** Solvers *)
+module Solver :
+sig
+  type solver 
+  type status = UNSATISFIABLE | UNKNOWN | SATISFIABLE
+      
+  val string_of_status : status -> string
 
   (** A string that describes all available solver parameters. *)
   val get_help : solver -> string
@@ -3081,7 +3086,7 @@ sig
       The unsat core is a subset of [Assertions]
       The result is empty if [Check] was not invoked before,
       if its results was not [UNSATISFIABLE], or if core production is disabled. *)
-  val get_unsat_core : solver -> AST.ast list
+  val get_unsat_core : solver -> Expr.expr list
 
   (** A brief justification of why the last call to [Check] returned [UNKNOWN]. *)
   val get_reason_unknown : solver -> string
@@ -3198,6 +3203,19 @@ sig
 
   (** Create a Fixedpoint context. *)
   val mk_fixedpoint : context -> fixedpoint
+
+  (** Retrieve statistics information from the last call to #Z3_fixedpoint_query. *)
+  val get_statistics : fixedpoint -> Statistics.statistics
+
+  (** Parse an SMT-LIB2 string with fixedpoint rules. 
+      Add the rules to the current fixedpoint context. 
+      Return the set of queries in the string. *)
+  val parse_string : fixedpoint -> string -> Expr.expr list
+
+  (** Parse an SMT-LIB2 file with fixedpoint rules. 
+      Add the rules to the current fixedpoint context. 
+      Return the set of queries in the file. *)
+  val parse_file : fixedpoint -> string -> Expr.expr list
 end
 
 (** Functions for handling SMT and SMT2 expressions and files *)
@@ -3272,12 +3290,12 @@ sig
   (** Gets an interpolant.
       For more information on interpolation please refer
       too the C/C++ API, which is well documented. *)
-  val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> AST.ASTVector.ast_vector
+  val get_interpolant : context -> Expr.expr -> Expr.expr -> Params.params -> Expr.expr list
 
   (** Computes an interpolant.
       For more information on interpolation please refer
       too the C/C++ API, which is well documented. *)
-  val compute_interpolant : context -> Expr.expr -> Params.params -> (AST.ASTVector.ast_vector * Model.model)
+  val compute_interpolant : context -> Expr.expr -> Params.params -> (Z3enums.lbool * Expr.expr list option * Model.model option)
 
   (** Retrieves an interpolation profile.
       For more information on interpolation please refer

src/api/z3_api.h

@@ -6022,7 +6022,7 @@ END_MLAPI_EXCLUDE
     /**
        \brief Parse an SMT-LIB2 string with fixedpoint rules. 
        Add the rules to the current fixedpoint context. 
-       Return the set of queries in the file.
+       Return the set of queries in the string.
 
        \param c - context.
        \param f - fixedpoint context.

src/ast/ast.cpp

@@ -316,6 +316,7 @@ func_decl::func_decl(symbol const & name, unsigned arity, sort * const * domain,
     decl(AST_FUNC_DECL, name, info),
     m_arity(arity),
     m_range(range) {
+    if (arity != 0)
         memcpy(const_cast<sort **>(get_domain()), domain, sizeof(sort *) * arity);
 }
 
@@ -378,7 +379,9 @@ quantifier::quantifier(bool forall, unsigned num_decls, sort * const * decl_sort
 
     memcpy(const_cast<sort **>(get_decl_sorts()), decl_sorts, sizeof(sort *) * num_decls);
     memcpy(const_cast<symbol*>(get_decl_names()), decl_names, sizeof(symbol) * num_decls);
+    if (num_patterns != 0)
         memcpy(const_cast<expr **>(get_patterns()), patterns, sizeof(expr *) * num_patterns);
+    if (num_no_patterns != 0)
         memcpy(const_cast<expr **>(get_no_patterns()), no_patterns, sizeof(expr *) * num_no_patterns);
 }
 

src/ast/fpa/fpa2bv_converter.cpp

@@ -48,19 +48,31 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
     SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP));
     SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP));
 
-    expr_ref sgn(m), s(m), e(m);
+    TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
-    m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), sgn);
+                    tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
-    m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), e);
+
-    m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), s);
+    expr_ref eq_sgn(m), eq_exp(m), eq_sig(m);
+    m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn);
+    m_simp.mk_eq(to_app(a)->get_arg(1), to_app(b)->get_arg(1), eq_exp);
+    m_simp.mk_eq(to_app(a)->get_arg(2), to_app(b)->get_arg(2), eq_sig);
+
+    dbg_decouple("fpa2bv_eq_sgn", eq_sgn);
+    dbg_decouple("fpa2bv_eq_exp", eq_exp);
+    dbg_decouple("fpa2bv_eq_sig", eq_sig);
+
+    expr_ref both_the_same(m);
+    m_simp.mk_and(eq_sgn, eq_exp, eq_sig, both_the_same);
+    dbg_decouple("fpa2bv_eq_both_the_same", both_the_same);
 
     // The SMT FPA theory asks for _one_ NaN value, but the bit-blasting
     // has many, like IEEE754. This encoding of equality makes it look like
     // a single NaN again. 
-    expr_ref both_the_same(m), a_is_nan(m), b_is_nan(m), both_are_nan(m);
+    expr_ref a_is_nan(m), b_is_nan(m), both_are_nan(m);    
-    m_simp.mk_and(sgn, s, e, both_the_same);
     mk_is_nan(a, a_is_nan);
     mk_is_nan(b, b_is_nan);
     m_simp.mk_and(a_is_nan, b_is_nan, both_are_nan);
+    dbg_decouple("fpa2bv_eq_both_are_nan", both_are_nan);
+
     m_simp.mk_or(both_are_nan, both_the_same, result);
 }
 
@@ -2051,6 +2063,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
         expr_ref sgn(m), sig(m), exp(m), lz(m);
         unpack(x, sgn, sig, exp, lz, true);
 
+        dbg_decouple("fpa2bv_to_float_x_sgn", sgn);
         dbg_decouple("fpa2bv_to_float_x_sig", sig);
         dbg_decouple("fpa2bv_to_float_x_exp", exp);
         dbg_decouple("fpa2bv_to_float_lz", lz);
@@ -2068,13 +2081,17 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
             // make sure that sig has at least to_sbits + 3
             res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits + 3 - from_sbits));
         }
-        else if (from_sbits >(to_sbits + 3)) {
+        else if (from_sbits > (to_sbits + 3)) {
             // collapse the extra bits into a sticky bit.
             expr_ref sticky(m), low(m), high(m);
-            low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig);
             high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig);
+            SASSERT(m_bv_util.get_bv_size(high) == to_sbits + 2);
+            low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig);            
             sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get());
+            SASSERT(m_bv_util.get_bv_size(sticky) == 1);
+            dbg_decouple("fpa2bv_to_float_sticky", sticky);
             res_sig = m_bv_util.mk_concat(high, sticky);            
+            SASSERT(m_bv_util.get_bv_size(res_sig) == to_sbits + 3);
         }
         else
             res_sig = sig;
@@ -2083,8 +2100,9 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
         unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
         SASSERT(sig_sz == to_sbits + 4);
 
-        expr_ref exponent_overflow(m);
+        expr_ref exponent_overflow(m), exponent_underflow(m);
         exponent_overflow = m.mk_false();
+        exponent_underflow = m.mk_false();
 
         if (from_ebits < (to_ebits + 2)) {
             res_exp = m_bv_util.mk_sign_extend(to_ebits - from_ebits + 2, exp);
@@ -2094,37 +2112,58 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
             lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz);
             res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
         }
-        else if (from_ebits >(to_ebits + 2)) {
+        else if (from_ebits > (to_ebits + 2)) {            
-            expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m);
+            expr_ref lz_rest(m), lz_redor(m), lz_redor_bool(m);            
-            expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m);
-            high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp);
-            low = m_bv_util.mk_extract(to_ebits + 1, 0, exp);
-            lows = m_bv_util.mk_extract(to_ebits + 1, to_ebits + 1, low);
-
-            high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get());
-            high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
-
-            zero1 = m_bv_util.mk_numeral(0, 1);
-            m_simp.mk_eq(high_red_and, one1, h_and_eq);
-            m_simp.mk_eq(high_red_or, zero1, h_or_eq);
-            m_simp.mk_eq(lows, zero1, s_is_zero);
-            m_simp.mk_eq(lows, one1, s_is_one);
-
-            expr_ref c2(m);
-            m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2);
-            m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow);
-
-            // Note: Upon overflow, we _could_ try to shift the significand around...
-
-            // subtract lz for subnormal numbers.
-            expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m);
-            lz_ext = m_bv_util.mk_extract(to_ebits + 1, 0, lz);
             lz_rest = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, lz);
             lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get());
             m_simp.mk_eq(lz_redor, one1, lz_redor_bool);
-            m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow);
+            dbg_decouple("fpa2bv_to_float_exp_lz_redor", lz_redor);
 
-            res_exp = m_bv_util.mk_bv_sub(low, lz_ext);
+            // subtract lz for subnormal numbers.
+            expr_ref exp_sub_lz(m);
+            exp_sub_lz = m_bv_util.mk_bv_sub(exp, lz);
+            dbg_decouple("fpa2bv_to_float_exp_sub_lz", exp_sub_lz);
+
+            expr_ref high(m), low(m), low_msb(m);
+            expr_ref no_ovf(m), zero1(m);
+            high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp_sub_lz);
+            low = m_bv_util.mk_extract(to_ebits + 1, 0, exp_sub_lz);
+            low_msb = m_bv_util.mk_extract(to_ebits + 1, to_ebits + 1, low);
+            dbg_decouple("fpa2bv_to_float_exp_high", high);
+            dbg_decouple("fpa2bv_to_float_exp_low", low);
+            dbg_decouple("fpa2bv_to_float_exp_low_msb", low_msb);
+            
+            res_exp = low;
+
+            expr_ref high_red_or(m), high_red_and(m);
+            high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get());
+            high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
+
+            expr_ref h_or_eq_0(m), h_and_eq_1(m), low_msb_is_one(m), low_msb_is_zero(m);
+            zero1 = m_bv_util.mk_numeral(0, 1);
+            m_simp.mk_eq(high_red_and, one1, h_and_eq_1);
+            m_simp.mk_eq(high_red_or, zero1, h_or_eq_0);
+            m_simp.mk_eq(low_msb, zero1, low_msb_is_zero);
+            m_simp.mk_eq(low_msb, one1, low_msb_is_one);
+            dbg_decouple("fpa2bv_to_float_exp_h_and_eq_1", h_and_eq_1);
+            dbg_decouple("fpa2bv_to_float_exp_h_or_eq_0", h_or_eq_0);
+            dbg_decouple("fpa2bv_to_float_exp_s_is_zero", low_msb_is_zero);
+            dbg_decouple("fpa2bv_to_float_exp_s_is_one", low_msb_is_one);
+            
+            m_simp.mk_and(h_or_eq_0, low_msb_is_one, exponent_underflow);
+            m_simp.mk_and(h_and_eq_1, low_msb_is_zero, exponent_overflow);
+            m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow);
+            dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow);
+            dbg_decouple("fpa2bv_to_float_exp_udf", exponent_underflow);
+
+            // exponent underflow means that the result is the smallest 
+            // representable float, rounded according to rm.            
+            m_simp.mk_ite(exponent_underflow, 
+                                m_bv_util.mk_concat(m_bv_util.mk_numeral(1, 1),
+                                                    m_bv_util.mk_numeral(1, to_ebits+1)), 
+                                res_exp, 
+                                res_exp);
+            m_simp.mk_ite(exponent_underflow, m_bv_util.mk_numeral(1, to_sbits+4), res_sig, res_sig);
         }
         else // from_ebits == (to_ebits + 2)
             res_exp = m_bv_util.mk_bv_sub(exp, lz);
@@ -2143,7 +2182,6 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
         m_simp.mk_eq(sgn, one1, is_neg);
         mk_ite(is_neg, ninf, pinf, sig_inf);
 
-        dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow);
         mk_ite(exponent_overflow, sig_inf, rounded, v6);        
 
         // And finally, we tie them together.
@@ -3044,13 +3082,6 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
     m_simp.mk_not(sig_is_zero, sig_is_not_zero);
     m_simp.mk_eq(exp, top_exp, exp_is_top);
     m_simp.mk_and(exp_is_top, sig_is_not_zero, result);
-
-    // Inject auxiliary lemmas that fix e to the one and only NaN value, 
-    // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
-    // has a value to propagate.
-    m_extra_assertions.push_back(m.mk_eq(sgn, m_bv_util.mk_numeral(0, 1)));
-    m_extra_assertions.push_back(m.mk_eq(exp, top_exp));
-    m_extra_assertions.push_back(m.mk_eq(sig, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(sig))));
 }
 
 void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {

src/interp/iz3translate.cpp

@@ -966,7 +966,7 @@ public:
         get_linear_coefficients(t,coeffs);
         if(coeffs.size() == 0)
             return make_int("1"); // arbitrary
-        rational d = coeffs[0];
+        rational d = abs(coeffs[0]);
         for(unsigned i = 1; i < coeffs.size(); i++){
             d = gcd(d,coeffs[i]);
         }

src/math/polynomial/polynomial.cpp

@@ -542,6 +542,7 @@ namespace polynomial {
                 increase_capacity(sz * 2);
             SASSERT(sz < m_capacity);
             m_ptr->m_size = sz;
+            if (sz == 0) return;
             memcpy(m_ptr->m_powers, pws, sizeof(power) * sz);
         }
         

src/math/simplex/sparse_matrix.h

@@ -79,7 +79,7 @@ namespace simplex {
             };
             col_entry(int r, int i): m_row_id(r), m_row_idx(i) {}
             col_entry(): m_row_id(0), m_row_idx(0) {}            
-            bool is_dead() const { return m_row_id == dead_id; }
+            bool is_dead() const { return (unsigned) m_row_id == dead_id; }
         };
      
         struct column;

src/math/simplex/sparse_matrix_def.h

@@ -79,7 +79,7 @@ namespace simplex {
     void sparse_matrix<Ext>::_row::del_row_entry(unsigned idx) {
         _row_entry & t = m_entries[idx];
         SASSERT(!t.is_dead());
-        t.m_next_free_row_entry_idx = m_first_free_idx;
+        t.m_next_free_row_entry_idx = (unsigned)m_first_free_idx;
         t.m_var = dead_id;
         m_size--;
         m_first_free_idx = idx;
@@ -513,8 +513,8 @@ namespace simplex {
             SASSERT(!m.is_zero(e.m_coeff));            
             SASSERT(e.m_var != dead_id);
             col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx];
-            SASSERT(c.m_row_id == row_id);
+            SASSERT((unsigned)c.m_row_id == row_id);
-            SASSERT(c.m_row_idx == i);
+            SASSERT((unsigned)c.m_row_idx == i);
             vars.insert(e.m_var);
         }                  
         int idx = r.m_first_free_idx;
@@ -544,7 +544,7 @@ namespace simplex {
             _row const& row = m_rows[c.m_row_id];
             _row_entry const& r = row.m_entries[c.m_row_idx];
             SASSERT(r.m_var == v); 
-            SASSERT(r.m_col_idx == i);
+            SASSERT((unsigned)r.m_col_idx == i);
             rows.insert(c.m_row_id);
         }                           
         int idx = col.m_first_free_idx;

src/muz/rel/dl_compiler.cpp

@@ -85,7 +85,7 @@ namespace datalog {
             removed_cols.size(), removed_cols.c_ptr(), result));
     }
 
-    void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
+    void compiler::make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
             reg_idx & result, bool reuse, instruction_block & acc) {
         relation_signature res_sig;
         relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig);
@@ -139,7 +139,7 @@ namespace datalog {
         return r;
     }
 
-    compiler::reg_idx compiler::get_single_column_register(const relation_sort & s) {
+    compiler::reg_idx compiler::get_single_column_register(const relation_sort s) {
         relation_signature singl_sig;
         singl_sig.push_back(s);
         return get_fresh_register(singl_sig);
@@ -165,7 +165,7 @@ namespace datalog {
         }
     }
 
-    void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort & s, const relation_element & val,
+    void compiler::make_add_constant_column(func_decl* head_pred, reg_idx src, const relation_sort s, const relation_element val,
             reg_idx & result, bool & dealloc, instruction_block & acc) {
         reg_idx singleton_table;
         if(!m_constant_registers.find(s, val, singleton_table)) {
@@ -185,7 +185,7 @@ namespace datalog {
         }
     }
 
-    void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, 
+    void compiler::make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
             bool & dealloc, instruction_block & acc) {
         
         TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
@@ -862,9 +862,11 @@ namespace datalog {
         ast_manager& m = m_context.get_manager();
         unsigned pt_len = r->get_positive_tail_size();
         unsigned ut_len = r->get_uninterpreted_tail_size();
-        if (pt_len == ut_len) {
+
+        // no negated predicates
+        if (pt_len == ut_len)
             return;
-        }
+
         // populate negative variables:
         for (unsigned i = pt_len; i < ut_len; ++i) {
             app * neg_tail = r->get_tail(i);

src/muz/rel/dl_compiler.h

@@ -135,7 +135,7 @@ namespace datalog {
 
         reg_idx get_fresh_register(const relation_signature & sig);
         reg_idx get_register(const relation_signature & sig, bool reuse, reg_idx r);
-        reg_idx get_single_column_register(const relation_sort & s);
+        reg_idx get_single_column_register(const relation_sort s);
 
         /**
            \brief Allocate registers for predicates in \c pred and add them into the \c regs map.
@@ -150,7 +150,7 @@ namespace datalog {
             const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc);
         void make_filter_interpreted_and_project(reg_idx src, app_ref & cond,
             const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc);
-        void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col,
+        void make_select_equal_and_project(reg_idx src, const relation_element val, unsigned col,
             reg_idx & result, bool reuse, instruction_block & acc);
         /**
            \brief Create add an union or widen operation and put it into \c acc.
@@ -174,10 +174,10 @@ namespace datalog {
 
         void make_dealloc_non_void(reg_idx r, instruction_block & acc);
 
-        void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort & s, const relation_element & val,
+        void make_add_constant_column(func_decl* pred, reg_idx src, const relation_sort s, const relation_element val,
             reg_idx & result, bool & dealloc, instruction_block & acc);
 
-        void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort & s, reg_idx & result, 
+        void make_add_unbound_column(rule* compiled_rule, unsigned col_idx, func_decl* pred, reg_idx src, const relation_sort s, reg_idx & result,
             bool & dealloc, instruction_block & acc);
         void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, 
             instruction_block & acc);

src/smt/params/smt_params_helper.pyg

@@ -45,6 +45,7 @@ def_module_params(module_name='smt',
                           ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
                           ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
                           ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'),
+                          ('arith.greatest_error_pivot', BOOL, False, 'Pivoting strategy'),
                           ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'),
                           ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
                           ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'),

src/smt/smt_justification.cpp

@@ -308,6 +308,7 @@ namespace smt {
         simple_justification(r, num_lits, lits),
         m_num_eqs(num_eqs) {
         m_eqs = new (r) enode_pair[num_eqs];
+        if (num_eqs != 0)
             memcpy(m_eqs, eqs, sizeof(enode_pair) * num_eqs);
         DEBUG_CODE({
             for (unsigned i = 0; i < num_eqs; i++) {

src/smt/theory_arith_core.h

@@ -2789,7 +2789,6 @@ namespace smt {
               tout << " --> ";
               ctx.display_detailed_literal(tout, l); 
               tout << "\n";);
-        SASSERT(false);
         if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) {
             literal_vector & lits = m_tmp_literal_vector2;
             lits.reset();

src/smt/theory_arith_int.h

@@ -777,8 +777,8 @@ namespace smt {
                         // u += ncoeff * lower_bound(v).get_rational();
                         u.addmul(ncoeff, lower_bound(v).get_rational());
                     }
-                    lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                    lower(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
-                    upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled());
+                    upper(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
                 }
                 else if (gcds.is_zero()) {
                     gcds = abs_ncoeff; 

src/tactic/fpa/fpa2bv_tactic.cpp

@@ -88,6 +88,22 @@ class fpa2bv_tactic : public tactic {
                     new_pr     = m.mk_modus_ponens(pr, new_pr);
                 }
                 g->update(idx, new_curr, new_pr, g->dep(idx));
+
+                if (is_app(new_curr)) {
+                    const app * a = to_app(new_curr.get());
+                    if (a->get_family_id() == m_conv.fu().get_family_id() &&
+                        a->get_decl_kind() == OP_FPA_IS_NAN) {
+                        // Inject auxiliary lemmas that fix e to the one and only NaN value, 
+                        // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation
+                        // has a value to propagate.
+                        expr * sgn, *sig, *exp;
+                        expr_ref top_exp(m);
+                        m_conv.split_fp(new_curr, sgn, exp, sig);
+                        m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1));
+                        m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)));
+                        m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig)));
+                    }
+                }
             }
 
             if (g->models_enabled())  

src/tactic/portfolio/default_tactic.cpp

@@ -36,8 +36,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
                                         cond(mk_is_qfbv_probe(),  mk_qfbv_tactic(m),
                                         cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m),                                        
-                                        cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m),
                                         cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
+                                        cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m),
                                         cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
                                         cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),
                                         cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),

src/test/polynomial_factorization.cpp

@@ -24,7 +24,8 @@ Notes:
 #include"polynomial_factorization.h"
 #endif
 
-using namespace std;
+using std::cout;
+using std::endl;
 
 // some prime numbers
 unsigned primes[] = {

src/util/hash.cpp

@@ -19,11 +19,18 @@ Revision History:
 
 #include"debug.h"
 #include"hash.h"
+#include <string.h>
+
+static unsigned read_unsigned(const char *s) {
+  unsigned n;
+  memcpy(&n, s, sizeof(unsigned));
+  return n;
+}
 
 // I'm using Bob Jenkin's hash function.
 // http://burtleburtle.net/bob/hash/doobs.html
 unsigned string_hash(const char * str, unsigned length, unsigned init_value) {
-    register unsigned a, b, c, len;
+    unsigned a, b, c, len;
 
     /* Set up the internal state */
     len = length;
@@ -31,10 +38,11 @@ unsigned string_hash(const char * str, unsigned length, unsigned init_value) {
     c = init_value;      /* the previous hash value */
 
     /*---------------------------------------- handle most of the key */
+    SASSERT(sizeof(unsigned) == 4);
     while (len >= 12) {
-        a += reinterpret_cast<const unsigned *>(str)[0];
+        a += read_unsigned(str);
-        b += reinterpret_cast<const unsigned *>(str)[1];
+        b += read_unsigned(str+4);
-        c += reinterpret_cast<const unsigned *>(str)[2];
+        c += read_unsigned(str+8);
         mix(a,b,c);
         str += 12; len -= 12;
     }

src/util/hwf.cpp

@@ -16,7 +16,9 @@ Author:
 Revision History:
 
 --*/
+#include<math.h>
 #include<float.h>
+#include<sstream>
 
 #ifdef _WINDOWS
 #pragma float_control( except, on )   // exception semantics; this does _not_ mean that exceptions are enabled (we want them off!)
@@ -24,19 +26,13 @@ Revision History:
 #pragma fp_contract(off)              // contractions off (`contraction' means x*y+z is turned into a fused-mul-add).
 #pragma fenv_access(on)               // fpu environment sensitivity (needed to be allowed to make FPU mode changes).
 #else
-#ifdef _WINDOWS
+#include<fenv.h>
-#pragma STDC FENV_ACCESS ON
-#endif
-#include <math.h>
-#include <fenv.h>
 #endif
 
 #ifndef _M_IA64
 #define USE_INTRINSICS
 #endif
 
-#include<sstream>
-
 #include"hwf.h"
 
 // Note:
@@ -310,13 +306,27 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co
     // CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium, 
     // Intel Sandybridge and AMD Bulldozers support that (via AVX).
 
+    set_rounding_mode(rm);
+
 #ifdef _M_IA64
     // IA64 (Itanium) will do it, if contractions are on.    
-    set_rounding_mode(rm);
     o.value = x.value * y.value + z.value;
 #else
-    set_rounding_mode(rm);
+#if defined(_WINDOWS)    
+#if _MSC_VER >= 1800
     o.value = ::fma(x.value, y.value, z.value);    
+#else // Windows, older than VS 2013
+  #ifdef USE_INTRINSICS
+      _mm_store_sd(&o.value, _mm_fmadd_sd(_mm_set_sd(x.value), _mm_set_sd(y.value), _mm_set_sd(z.value)));
+  #else
+      // If all else fails, we are imprecise.
+      o.value = (x.value * y.value) + z;
+  #endif
+#endif
+#else
+    // Linux, OSX
+    o.value = ::fma(x.value, y.value, z.value);
+#endif
 #endif
 }
 

src/util/inf_int_rational.cpp

@@ -19,9 +19,9 @@ Revision History:
 #include<sstream>
 #include"inf_int_rational.h"
 
-inf_int_rational inf_int_rational::m_zero(0);
+inf_int_rational inf_int_rational::m_zero;
-inf_int_rational inf_int_rational::m_one(1);
+inf_int_rational inf_int_rational::m_one;
-inf_int_rational inf_int_rational::m_minus_one(-1);
+inf_int_rational inf_int_rational::m_minus_one;
 
 std::string inf_int_rational::to_string() const {
     if (m_second == 0) {
@@ -39,3 +39,22 @@ std::string inf_int_rational::to_string() const {
     return s.str();
 }
 
+void initialize_inf_int_rational() {
+  inf_int_rational::init();
+}
+
+void inf_int_rational::init() {
+  m_zero.m_first = rational::zero();
+  m_one.m_first = rational::one();
+  m_minus_one.m_first = rational::minus_one();
+}
+
+void finalize_inf_int_rational() {
+  inf_int_rational::finalize();
+}
+
+void inf_int_rational::finalize() {
+  m_zero.~inf_int_rational();
+  m_one.~inf_int_rational();
+  m_minus_one.~inf_int_rational();
+}

src/util/inf_int_rational.h

@@ -33,6 +33,8 @@ class inf_int_rational {
     rational m_first;
     int      m_second;
  public:
+    static void init(); // called from rational::initialize() only
+    static void finalize();  // called from rational::finalize() only
 
     unsigned hash() const { 
         return m_first.hash() ^ (static_cast<unsigned>(m_second) + 1);
@@ -272,7 +274,7 @@ class inf_int_rational {
             if (r.m_second >= 0) {
                 return r.m_first;
             }
-            return r.m_first - rational(1);
+            return r.m_first - rational::one();
         }
         
         return floor(r.m_first);
@@ -283,7 +285,7 @@ class inf_int_rational {
             if (r.m_second <= 0) {
                 return r.m_first;
             }
-            return r.m_first + rational(1);
+            return r.m_first + rational::one();
         }
         
         return ceil(r.m_first);

src/util/inf_rational.cpp

@@ -18,9 +18,9 @@ Revision History:
 --*/
 #include"inf_rational.h"
 
-inf_rational inf_rational::m_zero(0);
+inf_rational inf_rational::m_zero;
-inf_rational inf_rational::m_one(1);
+inf_rational inf_rational::m_one;
-inf_rational inf_rational::m_minus_one(-1);
+inf_rational inf_rational::m_minus_one;
 
 inf_rational inf_mult(inf_rational const& r1, inf_rational const& r2) 
 {
@@ -128,7 +128,7 @@ inf_rational inf_power(inf_rational const& r, unsigned n)
         // 0 will work.
     }
     else if (r.m_first.is_zero()) {
-        result.m_first = rational(-1);        
+        result.m_first = rational::minus_one();
     }
     else if (r.m_first.is_pos()) {
         result.m_first = rational(r.m_first - r.m_first/rational(2)).expt(n);
@@ -152,7 +152,7 @@ inf_rational sup_power(inf_rational const& r, unsigned n)
         result.m_first = r.m_first.expt(n);
     }
     else if (r.m_first.is_zero() || (n == 0)) {
-        result.m_first = rational(1);        
+        result.m_first = rational::one();
     }
     else if (r.m_first.is_pos() || is_even) {
         result.m_first = rational(r.m_first + r.m_first/rational(2)).expt(n);
@@ -177,3 +177,23 @@ inf_rational sup_root(inf_rational const& r, unsigned n)
     // use r.
     return r;
 }
+
+void initialize_inf_rational() {
+    inf_rational::init();
+}
+
+void inf_rational::init() {
+    m_zero.m_first = rational::zero();
+    m_one.m_first = rational::one();
+    m_minus_one.m_first = rational::minus_one();
+}
+
+void finalize_inf_rational() {
+    inf_rational::finalize();
+}
+
+void inf_rational::finalize() {
+    m_zero.~inf_rational();
+    m_one.~inf_rational();
+    m_minus_one.~inf_rational();
+}

src/util/inf_rational.h

@@ -33,6 +33,8 @@ class inf_rational {
     rational m_first;
     rational m_second;
  public:
+    static void init(); // called from rational::initialize() only
+    static void finalize();  // called from rational::finalize() only
 
     unsigned hash() const { 
         return m_first.hash() ^ (m_second.hash()+1);
@@ -82,7 +84,7 @@ class inf_rational {
 
     explicit inf_rational(rational const& r, bool pos_inf):
         m_first(r),
-        m_second(pos_inf?rational(1):rational(-1))
+        m_second(pos_inf ? rational::one() : rational::minus_one())
     {}
 
     inf_rational(rational const& r):
@@ -313,7 +315,7 @@ class inf_rational {
             if (r.m_second.is_nonneg()) {
                 return r.m_first;
             }
-            return r.m_first - rational(1);
+            return r.m_first - rational::one();
         }
         
         return floor(r.m_first);
@@ -324,7 +326,7 @@ class inf_rational {
             if (r.m_second.is_nonpos()) {
                 return r.m_first;
             }
-            return r.m_first + rational(1);
+            return r.m_first + rational::one();
         }
         
         return ceil(r.m_first);

src/util/mpf.cpp

@@ -348,7 +348,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
             bool sticky = false;
             while (ds < 0)
             {
-                if (!m_mpz_manager.is_even(o.significand)) sticky = true;
+                sticky |= m_mpz_manager.is_odd(o.significand);
                 m_mpz_manager.machine_div2k(o.significand, 1);            
                 ds++;
             }

src/util/rational.cpp

@@ -29,9 +29,9 @@ rational             rational::m_one;
 rational             rational::m_minus_one;
 vector<rational>     rational::m_powers_of_two;
 
-void mk_power_up_to(vector<rational> & pws, unsigned n) {
+static void mk_power_up_to(vector<rational> & pws, unsigned n) {
     if (pws.empty()) {
-        pws.push_back(rational(1));
+        pws.push_back(rational::one());
     }
     unsigned sz = pws.size();
     rational curr = pws[sz - 1];
@@ -53,16 +53,28 @@ rational rational::power_of_two(unsigned k) {
     return result;
 }
 
+// in inf_rational.cpp
+void initialize_inf_rational();
+void finalize_inf_rational();
+
+// in inf_int_rational.cpp
+void initialize_inf_int_rational();
+void finalize_inf_int_rational();
+
 void rational::initialize() {
     if (!g_mpq_manager) {
         g_mpq_manager = alloc(synch_mpq_manager);
         m().set(m_zero.m_val, 0);
         m().set(m_one.m_val, 1);
         m().set(m_minus_one.m_val, -1);
+        initialize_inf_rational();
+        initialize_inf_int_rational();
     }
 }
 
 void rational::finalize() {
+    finalize_inf_rational();
+    finalize_inf_int_rational();
     m_powers_of_two.finalize();
     m_zero.~rational();
     m_one.~rational();