Merge branch 'master' of https://github.com/Z3Prover/z3

src/api/java/AST.java

@@ -33,7 +33,7 @@ public class AST extends Z3Object implements Comparable
     {
         AST casted = null;
 
-	try
+        try
         {
             casted = AST.class.cast(o);
         } catch (ClassCastException e)
@@ -41,13 +41,12 @@ public class AST extends Z3Object implements Comparable
             return false;
         }
 
-	return  
+        return  (this == casted) ||
-	    (this == casted) || 
+                (this != null) &&
-	    (this != null) &&
+                (casted != null) &&
-	    (casted != null) &&
+                (getContext().nCtx() == casted.getContext().nCtx()) &&
-	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+                (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
-	    (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
+    }
-}
 
     /**
      * Object Comparison. 

src/api/java/Constructor.java

@@ -80,11 +80,20 @@ public class Constructor extends Z3Object
 
     /**
      * Destructor.
+     * @throws Throwable 
      * @throws Z3Exception on error
      **/
-    protected void finalize()
+    protected void finalize() throws Throwable
     {
-        Native.delConstructor(getContext().nCtx(), getNativeObject());
+        try {
+            Native.delConstructor(getContext().nCtx(), getNativeObject());
+        }
+        catch (Throwable t) {
+            throw t;
+        }
+        finally {
+            super.finalize();
+        }
     }
 
     private int n = 0;

src/api/java/ConstructorList.java

@@ -24,11 +24,20 @@ public class ConstructorList extends Z3Object
 {
     /**
      * Destructor.
+     * @throws Throwable 
      * @throws Z3Exception on error
      **/
-    protected void finalize()
+    protected void finalize() throws Throwable
     {
-        Native.delConstructorList(getContext().nCtx(), getNativeObject());
+        try {        
+            Native.delConstructorList(getContext().nCtx(), getNativeObject());            
+        }
+        catch (Throwable t) {
+            throw t;
+        }
+        finally {
+            super.finalize();
+        }
     }
 
     ConstructorList(Context ctx, long obj)

src/api/java/Context.java

@@ -18,6 +18,7 @@ Notes:
 package com.microsoft.z3;
 
 import java.util.Map;
+import java.util.concurrent.atomic.AtomicInteger;
 
 import com.microsoft.z3.enumerations.Z3_ast_print_mode;
 
@@ -3766,29 +3767,35 @@ public class Context extends IDisposable
         return m_Optimize_DRQ;
     }
 
-    protected long m_refCount = 0;
+    protected AtomicInteger m_refCount = new AtomicInteger(0);
 
     /**
      * Finalizer.
+     * @throws Throwable 
      **/
-    protected void finalize()
+    protected void finalize() throws Throwable
     {
-        dispose();
+        try {            
-
+            dispose();
-        if (m_refCount == 0)
+    
-        {
+            if (m_refCount.get() == 0)
-            try
             {
-                Native.delContext(m_ctx);
+                try
-            } catch (Z3Exception e)
+                {
-            {
+                    Native.delContext(m_ctx);
-                // OK.
+                } catch (Z3Exception e)
-            }
+                {
-            m_ctx = 0;
+                    // OK.
-        } 
+                }
-        /*
+                m_ctx = 0;
-        else
+            } 
-            CMW: re-queue the finalizer? */
+        }
+        catch (Throwable t) {
+            throw t;
+        }
+        finally {
+            super.finalize();
+        }
     }
 
     /**

src/api/java/Z3Object.java

@@ -25,10 +25,19 @@ public class Z3Object extends IDisposable
 {
     /**
      * Finalizer.
+     * @throws Throwable 
      **/
-    protected void finalize()
+    protected void finalize() throws Throwable
     {
-        dispose();
+        try {
+            dispose();            
+        }
+        catch (Throwable t) {
+            throw t;
+        }
+        finally {
+            super.finalize();
+        }
     }
 
     /**
@@ -43,8 +52,8 @@ public class Z3Object extends IDisposable
         }
 
         if (m_ctx != null)
-        {
+        {            
-            m_ctx.m_refCount--;
+            m_ctx.m_refCount.decrementAndGet();
             m_ctx = null;
         }
     }
@@ -54,13 +63,13 @@ public class Z3Object extends IDisposable
 
     Z3Object(Context ctx)
     {
-        ctx.m_refCount++;
+        ctx.m_refCount.incrementAndGet();
         m_ctx = ctx;
     }
 
     Z3Object(Context ctx, long obj)
     {
-        ctx.m_refCount++;
+        ctx.m_refCount.incrementAndGet();
         m_ctx = ctx;
         incRef(obj);
         m_n_obj = obj;

src/smt/theory_diff_logic.h

@@ -399,7 +399,6 @@ namespace smt {
     };
 
     struct sidl_ext {
-        // TODO: It doesn't need to be a rational, but a bignum integer.
         static const bool m_int_theory = true;
         typedef s_integer numeral;
         typedef s_integer fin_numeral;
@@ -415,13 +414,11 @@ namespace smt {
         rdl_ext() : m_epsilon(rational(), true) {}
     };
 
-    struct srdl_ext {
+    //
-        static const bool m_int_theory = false;
+    // there is no s_rational class, so 
-        typedef inf_s_integer numeral;
+    // instead we use multi-precision rationals.
-        typedef s_integer fin_numeral;
+    //
-        numeral m_epsilon;
+    struct srdl_ext : public rdl_ext {};
-        srdl_ext() : m_epsilon(s_integer(0),true) {}
-    };
 
     typedef theory_diff_logic<idl_ext>  theory_idl;
     typedef theory_diff_logic<sidl_ext> theory_fidl;