Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

RELEASE_NOTES

@@ -61,6 +61,8 @@ Version 4.3.2
 
 - Fixed bugs in the C++ API (Thanks to Andrey Kupriyanov).
 
+- Fixed bug reported at http://z3.codeplex.com/workitem/23 (Thanks to Paul Jackson).
+
 Version 4.3.1
 =============
 

scripts/mk_util.py

@@ -33,6 +33,7 @@ LDFLAGS=getenv("LDFLAGS", "")
 JAVA=getenv("JAVA", "java")
 JAVAC=getenv("JAVAC", "javac")
 JAVA_HOME=getenv("JAVA_HOME", None)
+JNI_HOME=getenv("JNI_HOME", None)
 
 CXX_COMPILERS=['g++', 'clang++']
 C_COMPILERS=['gcc', 'clang']
@@ -222,6 +223,7 @@ def check_java():
     if r != 0:
         raise MKException('Failed testing Java program. Set environment variable JAVA with the path to the Java virtual machine')
     find_java_home()
+    find_jni_home()
 
 def find_jni_h(path):
     for root, dirs, files in os.walk(path): 
@@ -233,9 +235,13 @@ def find_jni_h(path):
 def find_java_home():
     global JAVA_HOME
     if JAVA_HOME != None:
-        if is_verbose():
+        if IS_WINDOWS:
-            print("Checking jni.h...")
+            ind = '%s%s' % (JAVA_HOME, '\\bin\\java.exe')
-        if os.path.exists(os.path.join(JAVA_HOME, 'include', 'jni.h')):
+        else:
+            ind = '%s%s' % (JAVA_HOME, '/bin/java')
+	if not os.path.exists(ind):
+            raise MKException("Failed to detect java at '%s'.Possible solution: set JAVA_HOME with the path to JDK." % os.path.join(JAVA_HOME))
+        else:
 	    return
     if is_verbose():
         print("Finding JAVA_HOME...")
@@ -252,20 +258,51 @@ def find_java_home():
         m = open_pat.match(line)
         if m:
             # Remove last 3 directives from m.group(1)
-            print(m.group(1))
             tmp  = m.group(1).split(os.sep)
             path = string.join(tmp[:len(tmp) - 3], os.sep)
-            if is_verbose():
+            if IS_WINDOWS:
-                print("Checking jni.h...")
+                ind = '%s%s' % (path, '\\bin\\java.exe')
-            jni_dir = find_jni_h(path)
+            else:
-            if not jni_dir:
+                ind = '%s%s' % (path, '/bin/java')
-                raise MKException("Failed to detect jni.h at '%s'.Possible solution: set JAVA_HOME with the path to JDK." % os.path.join(path, 'include'))
+            if os.path.exists(ind): 
-            JAVA_HOME = os.path.split(jni_dir)[0]
+		JAVA_HOME = path
-            if is_verbose():
+		return
-                print('JAVA_HOME=%s' % JAVA_HOME)
+	    if IS_OSX:
+                path = '%s%s' % (path, '/Contents/Home/')
+                ind = '%s%s' % (path, 'bin/java')
+                if os.path.exists(ind): 
+		    JAVA_HOME = path
+		    return
+            raise MKException("Failed to detect java at '%s'.Possible solution: set JAVA_HOME with the path to JDK." % os.path.join(path))
             return
     raise MKException('Failed to find JAVA_HOME')
 
+def find_jni_home():
+    global JNI_HOME
+    if JNI_HOME != None:
+        if is_verbose():
+            print("Checking jni.h...")
+	path = JNI_HOME
+        fn = os.path.join(path, 'jni.h')
+        print("Checking for jni.h in %s..." % JNI_HOME)
+        if os.path.exists(fn):
+            return
+    else:
+        path = '%s%s' % (JAVA_HOME, '/include/')
+        fn = '%s%s' % (path, 'jni.h')
+        print("Checking for jni.h in %s..." % path)
+        if os.path.exists(fn):
+            JNI_HOME = find_jni_h(path)
+        elif IS_OSX:
+            # Apparently Apple knows best where to put stuff...
+            path = '/System/Library/Frameworks/JavaVM.framework/Headers/'
+            fn = '%s%s' % (path, 'jni.h')
+            print("Checking for jni.h in %s..." % path)
+            if os.path.exists(fn):
+                JNI_HOME = find_jni_h(path)
+    if JNI_HOME == None:
+        raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
+
 def is64():
     return sys.maxsize >= 2**32
 
@@ -402,6 +439,7 @@ def display_help(exit_code):
     print("  JAVA       Java virtual machine (only relevant if -j or --java option is provided)")
     print("  JAVAC      Java compiler (only relevant if -j or --java option is provided)")
     print("  JAVA_HOME  JDK installation directory (only relevant if -j or --java option is provided)")
+    print("  JNI_HOME   JNI bindings directory (only relevant if -j or --java option is provided)")
     exit(exit_code)
 
 # Parse configuration option for mk_make script
@@ -1086,7 +1124,7 @@ class JavaDLLComponent(Component):
             mk_dir(os.path.join(BUILD_DIR, 'api', 'java', 'classes'))
             dllfile = '%s$(SO_EXT)' % self.dll_name            
             out.write('libz3java$(SO_EXT): libz3$(SO_EXT) %s\n' % os.path.join(self.to_src_dir, 'Native.cpp'))
-            t = '\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/java/Native$(OBJ_EXT) -I"%s/include" -I"%s/include/PLATFORM" -I%s %s/Native.cpp\n' % (JAVA_HOME, JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir)
+            t = '\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)api/java/Native$(OBJ_EXT) -I"%s" -I"%s/PLATFORM" -I%s %s/Native.cpp\n' % (JNI_HOME, JNI_HOME, get_component('api').to_src_dir, self.to_src_dir)
             if IS_OSX:
                 t = t.replace('PLATFORM', 'darwin')
             elif IS_LINUX:
@@ -1236,7 +1274,7 @@ class JavaExampleComponent(ExampleComponent):
     def mk_makefile(self, out):
         if JAVA_ENABLED:
             pkg = get_component(JAVA_COMPONENT).package_name + '.jar'
-            out.write('_ex_%s: %s' % (self.name, pkg))
+            out.write('JavaExample.class: %s' % (pkg))
             deps = ''
             for jfile in get_java_files(self.ex_dir):
                 out.write(' %s' % os.path.join(self.to_ex_dir, jfile))
@@ -1248,7 +1286,8 @@ class JavaExampleComponent(ExampleComponent):
             for javafile in get_java_files(self.ex_dir):
                 out.write(' ')
                 out.write(os.path.join(win_ex_dir, javafile))
-            out.write(' -d .\n\n')
+            out.write(' -d .\n')
+            out.write('_ex_%s: JavaExample.class\n\n' % (self.name))
 
 class PythonExampleComponent(ExampleComponent):
     def __init__(self, name, path):
@@ -1387,6 +1426,7 @@ def mk_config():
             print('64-bit:         %s' % is64())
             if is_java_enabled():
                 print('Java Home:      %s' % JAVA_HOME)
+                print('JNI Home:       %s' % JNI_HOME)
                 print('Java Compiler:  %s' % JAVAC)
                 print('Java VM:        %s' % JAVA)
     else:
@@ -1491,6 +1531,7 @@ def mk_config():
             print('Python version: %s' % distutils.sysconfig.get_python_version())
             if is_java_enabled():
                 print('Java Home:      %s' % JAVA_HOME)
+                print('JNI Home:       %s' % JNI_HOME)
                 print('Java Compiler:  %s' % JAVAC)
                 print('Java VM:        %s' % JAVA)
 

src/api/dotnet/Constructor.cs

@@ -35,7 +35,6 @@ namespace Microsoft.Z3
         {
             get
             {                
-                init();
                 return n;
             }
         }
@@ -48,8 +47,11 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                init();
+                IntPtr constructor = IntPtr.Zero;
-                return m_constructorDecl;
+                IntPtr tester = IntPtr.Zero;
+                IntPtr[] accessors = new IntPtr[n];
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
+                return new FuncDecl(Context, constructor);                
             }
         }
 
@@ -61,8 +63,11 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                init();
+                IntPtr constructor = IntPtr.Zero;
-                return m_testerDecl;
+                IntPtr tester = IntPtr.Zero;
+                IntPtr[] accessors = new IntPtr[n];
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
+                return new FuncDecl(Context, tester);                
             }
         }
 
@@ -74,8 +79,14 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-                init(); 
+                IntPtr constructor = IntPtr.Zero;
-                return m_accessorDecls;
+                IntPtr tester = IntPtr.Zero;
+                IntPtr[] accessors = new IntPtr[n];
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);                
+                FuncDecl[] t = new FuncDecl[n];
+                for (uint i = 0; i < n; i++)
+                    t[i] = new FuncDecl(Context, accessors[i]); 
+                return t;
             }
         }
 
@@ -87,22 +98,8 @@ namespace Microsoft.Z3
             Native.Z3_del_constructor(Context.nCtx, NativeObject);
         }        
 
-        #region Object invariant
-
-        [ContractInvariantMethod]
-        private void ObjectInvariant()
-        {
-            Contract.Invariant(m_testerDecl == null || m_constructorDecl != null);
-            Contract.Invariant(m_testerDecl == null || m_accessorDecls != null);
-        }
-
-        #endregion
-
         #region Internal
-        readonly private uint n = 0;
+        private uint n = 0;
-        private FuncDecl m_testerDecl = null;
-        private FuncDecl m_constructorDecl = null;
-        private FuncDecl[] m_accessorDecls = null;
         
         internal Constructor(Context ctx, Symbol name, Symbol recognizer, Symbol[] fieldNames,
                              Sort[] sorts, uint[] sortRefs)
@@ -129,24 +126,6 @@ namespace Microsoft.Z3
 
         }
 
-        private void init()
-        {
-            Contract.Ensures(m_constructorDecl != null);
-            Contract.Ensures(m_testerDecl != null);
-            Contract.Ensures(m_accessorDecls != null);
-
-            if (m_testerDecl != null) return;
-            IntPtr constructor = IntPtr.Zero;
-            IntPtr tester = IntPtr.Zero;
-            IntPtr[] accessors = new IntPtr[n];
-            Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
-            m_constructorDecl = new FuncDecl(Context, constructor);
-            m_testerDecl = new FuncDecl(Context, tester);
-            m_accessorDecls = new FuncDecl[n];
-            for (uint i = 0; i < n; i++)
-                m_accessorDecls[i] = new FuncDecl(Context, accessors[i]);
-        }
-
         #endregion
     }
 }

src/api/dotnet/EnumSort.cs

@@ -36,8 +36,11 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
+                uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
-                return _constdecls;
+                FuncDecl[] t = new FuncDecl[n];
+                for (uint i = 0; i < n; i++)
+                    t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
+                return t;                
             }
         }
 
@@ -49,8 +52,11 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<Expr[]>() != null);
-
+                FuncDecl[] cds = ConstDecls;
-                return _consts;
+                Expr[] t = new Expr[cds.Length];
+                for (uint i = 0; i < t.Length; i++)
+                    t[i] = Context.MkApp(cds[i]);
+                return t;
             }
         }
 
@@ -62,28 +68,15 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
+                uint n = Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject);
-                return _testerdecls;
+                FuncDecl[] t = new FuncDecl[n];
+                for (uint i = 0; i < n; i++)
+                    t[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
+                return t;
             }
         }
 
-        #region Object Invariant
-
-        [ContractInvariantMethod]
-        private void ObjectInvariant()
-        {
-            Contract.Invariant(this._constdecls != null);
-            Contract.Invariant(this._testerdecls != null);
-            Contract.Invariant(this._consts != null);
-        }
-
-
-        #endregion
-
         #region Internal
-        readonly private FuncDecl[] _constdecls = null, _testerdecls = null;
-        readonly private Expr[] _consts = null;
-
         internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
             : base(ctx)
         {
@@ -96,15 +89,6 @@ namespace Microsoft.Z3
             IntPtr[] n_testers = new IntPtr[n];
             NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
                                                          Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
-            _constdecls = new FuncDecl[n];
-            for (uint i = 0; i < n; i++)
-                _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
-            _testerdecls = new FuncDecl[n];
-            for (uint i = 0; i < n; i++)
-                _testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
-            _consts = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                _consts[i] = ctx.MkApp(_constdecls[i]);
         }
         #endregion
     };

src/api/dotnet/ListSort.cs

@@ -36,7 +36,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return nilDecl;
+                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0));                                
             }
         }
 
@@ -48,7 +48,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<Expr>() != null);
-                return nilConst;
+                return Context.MkApp(NilDecl);
             }
         }
 
@@ -60,7 +60,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return isNilDecl;
+                return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0));
             }
         }
 
@@ -72,7 +72,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return consDecl;
+                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1));
             }
         }
 
@@ -85,7 +85,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return isConsDecl;
+                return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1));
             }
         }
 
@@ -97,7 +97,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return headDecl;
+                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0));
             }
         }
 
@@ -109,31 +109,11 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return tailDecl;
+                return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1));
             }
         }
 
-        #region Object Invariant
-
-        [ContractInvariantMethod]
-        private void ObjectInvariant()
-        {
-            Contract.Invariant(nilConst != null);
-            Contract.Invariant(nilDecl != null);
-            Contract.Invariant(isNilDecl != null);
-            Contract.Invariant(consDecl != null);
-            Contract.Invariant(isConsDecl != null);
-            Contract.Invariant(headDecl != null);
-            Contract.Invariant(tailDecl != null);
-        }
-
-
-        #endregion
-
         #region Internal        
-        readonly private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
-        readonly private Expr nilConst;
-
         internal ListSort(Context ctx, Symbol name, Sort elemSort)
             : base(ctx)
         {
@@ -141,22 +121,12 @@ namespace Microsoft.Z3
             Contract.Requires(name != null);
             Contract.Requires(elemSort != null);
 
-            IntPtr inil = IntPtr.Zero,
+            IntPtr inil = IntPtr.Zero, iisnil = IntPtr.Zero, 
-                   iisnil = IntPtr.Zero,
+                   icons = IntPtr.Zero, iiscons = IntPtr.Zero,
-                   icons = IntPtr.Zero,
+                   ihead = IntPtr.Zero, itail = IntPtr.Zero;
-                   iiscons = IntPtr.Zero,
-                   ihead = IntPtr.Zero,
-                   itail = IntPtr.Zero;
 
             NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
                                                   ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);            
-            nilDecl = new FuncDecl(ctx, inil);
-            isNilDecl = new FuncDecl(ctx, iisnil);
-            consDecl = new FuncDecl(ctx, icons);
-            isConsDecl = new FuncDecl(ctx, iiscons);
-            headDecl = new FuncDecl(ctx, ihead);
-            tailDecl = new FuncDecl(ctx, itail);
-            nilConst = ctx.MkConst(nilDecl);
         }
         #endregion
     };

src/api/java/Constructor.java

@@ -17,7 +17,6 @@ public class Constructor extends Z3Object
 	 **/
 	public int getNumFields() throws Z3Exception
 	{	
-		init();
 		return n;
 	}
 
@@ -27,8 +26,11 @@ public class Constructor extends Z3Object
 	 **/
 	public FuncDecl ConstructorDecl() throws Z3Exception
 	{
-		init();
+	    Native.LongPtr constructor = new Native.LongPtr();
-		return m_constructorDecl;
+	    Native.LongPtr tester = new Native.LongPtr();
+	    long[] accessors = new long[n];
+        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
+        return new FuncDecl(getContext(), constructor.value);         
 	}
 
 	/**
@@ -37,8 +39,11 @@ public class Constructor extends Z3Object
 	 **/
 	public FuncDecl getTesterDecl() throws Z3Exception
 	{
-		init();
+	    Native.LongPtr constructor = new Native.LongPtr();
-		return m_testerDecl;
+        Native.LongPtr tester = new Native.LongPtr();
+        long[] accessors = new long[n];
+        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
+        return new FuncDecl(getContext(), tester.value);
 	}
 
 	/**
@@ -47,8 +52,14 @@ public class Constructor extends Z3Object
 	 **/
 	public FuncDecl[] getAccessorDecls() throws Z3Exception
 	{
-		init();
+	    Native.LongPtr constructor = new Native.LongPtr();
-		return m_accessorDecls;
+        Native.LongPtr tester = new Native.LongPtr();
+        long[] accessors = new long[n];
+        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
+        FuncDecl[] t = new FuncDecl[n];
+        for (int i = 0; i < n; i++)
+            t[i] = new FuncDecl(getContext(), accessors[i]); 
+        return t;
 	}
 
 	/**
@@ -60,9 +71,6 @@ public class Constructor extends Z3Object
 	}
 
 	private int n = 0;
-	private FuncDecl m_testerDecl = null;
-	private FuncDecl m_constructorDecl = null;
-	private FuncDecl[] m_accessorDecls = null;
 
 	Constructor(Context ctx, Symbol name, Symbol recognizer,
 			Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
@@ -87,21 +95,4 @@ public class Constructor extends Z3Object
 				Sort.arrayToNative(sorts), sortRefs));
 
 	}
-
-	private void init() throws Z3Exception
-	{
-		if (m_testerDecl != null)
-			return;
-		Native.LongPtr constructor = new Native.LongPtr();
-		Native.LongPtr tester = new Native.LongPtr();
-		long[] accessors = new long[n];
-		Native.queryConstructor(getContext().nCtx(), getNativeObject(), n,
-				constructor, tester, accessors);
-		m_constructorDecl = new FuncDecl(getContext(), constructor.value);
-		m_testerDecl = new FuncDecl(getContext(), tester.value);
-		m_accessorDecls = new FuncDecl[n];
-		for (int i = 0; i < n; i++)
-			m_accessorDecls[i] = new FuncDecl(getContext(), accessors[i]);
-	}
-
 }

src/api/java/EnumSort.java

@@ -14,30 +14,39 @@ public class EnumSort extends Sort
 	/**
 	 * The function declarations of the constants in the enumeration.
 	 **/
-	public FuncDecl[] getConstDecls()
+	public FuncDecl[] getConstDecls() throws Z3Exception
 	{
-		return _constdecls;
+	    int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
+        FuncDecl[] t = new FuncDecl[n];
+        for (int i = 0; i < n; i++)
+            t[i] = new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), i));
+        return t;
 	}
 
 	/**
 	 * The constants in the enumeration.
 	 **/
-	public Expr[] getConsts()
+	public Expr[] getConsts() throws Z3Exception
 	{	    
-		return _consts;
+	    FuncDecl[] cds = getConstDecls();
+        Expr[] t = new Expr[cds.length];
+        for (int i = 0; i < t.length; i++)
+            t[i] = getContext().mkApp(cds[i]);
+        return t;
 	}
 
 	/**
 	 * The test predicates for the constants in the enumeration.
 	 **/
-	public FuncDecl[] getTesterDecls()
+	public FuncDecl[] getTesterDecls() throws Z3Exception
 	{
-		return _testerdecls;
+	    int n = Native.getDatatypeSortNumConstructors(getContext().nCtx(), getNativeObject());
+        FuncDecl[] t = new FuncDecl[n];
+        for (int i = 0; i < n; i++)
+            t[i] = new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), i));
+        return t;
 	}
 
-	private FuncDecl[] _constdecls = null, _testerdecls = null;
-	private Expr[] _consts = null;
-
 	EnumSort(Context ctx, Symbol name, Symbol[] enumNames) throws Z3Exception
 	{
 		super(ctx);
@@ -48,14 +57,5 @@ public class EnumSort extends Sort
 		setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
 				name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
 				n_constdecls, n_testers));		
-		_constdecls = new FuncDecl[n];
-		for (int i = 0; i < n; i++)
-		    _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
-		_testerdecls = new FuncDecl[n];
-		for (int i = 0; i < n; i++)
-		    _testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
-		_consts = new Expr[n];
-		for (int i = 0; i < n; i++)
-		    _consts[i] = ctx.mkApp(_constdecls[i], (Expr[])null);
 	}
 };

src/api/java/ListSort.java

@@ -13,65 +13,68 @@ public class ListSort extends Sort
 {
     /**
      * The declaration of the nil function of this list sort.
+     * @throws Z3Exception 
      **/
-    public FuncDecl getNilDecl()
+    public FuncDecl getNilDecl() throws Z3Exception
     {
-        return nilDecl;
+        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 0));
     }
 
     /**
      * The empty list.
+     * @throws Z3Exception 
      **/
-    public Expr getNil()
+    public Expr getNil() throws Z3Exception
     {
-        return nilConst;
+        return getContext().mkApp(getNilDecl());
     }
 
     /**
      * The declaration of the isNil function of this list sort.
+     * @throws Z3Exception 
      **/
-    public FuncDecl getIsNilDecl()
+    public FuncDecl getIsNilDecl() throws Z3Exception
     {
-        return isNilDecl;
+        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 0));
     }
 
     /**
      * The declaration of the cons function of this list sort.
+     * @throws Z3Exception 
      **/
-    public FuncDecl getConsDecl()
+    public FuncDecl getConsDecl() throws Z3Exception
     {
-        return consDecl;
+        return new FuncDecl(getContext(), Native.getDatatypeSortConstructor(getContext().nCtx(), getNativeObject(), 1));
     }
 
     /**
      * The declaration of the isCons function of this list sort.
+     * @throws Z3Exception 
      * 
      **/
-    public FuncDecl getIsConsDecl()
+    public FuncDecl getIsConsDecl() throws Z3Exception
     {
-        return isConsDecl;
+        return new FuncDecl(getContext(), Native.getDatatypeSortRecognizer(getContext().nCtx(), getNativeObject(), 1));
     }
 
     /**
      * The declaration of the head function of this list sort.
+     * @throws Z3Exception 
      **/
-    public FuncDecl getHeadDecl()
+    public FuncDecl getHeadDecl() throws Z3Exception
     {
-        return headDecl;
+        return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 0));
     }
 
     /**
      * The declaration of the tail function of this list sort.
+     * @throws Z3Exception 
      **/
-    public FuncDecl getTailDecl()
+    public FuncDecl getTailDecl() throws Z3Exception
     {
-        return tailDecl;
+        return new FuncDecl(getContext(), Native.getDatatypeSortConstructorAccessor(getContext().nCtx(), getNativeObject(), 1, 1));
     }
 
-    private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl,
-            tailDecl;
-    private Expr nilConst;
-
     ListSort(Context ctx, Symbol name, Sort elemSort) throws Z3Exception
     {
         super(ctx);
@@ -83,12 +86,5 @@ public class ListSort extends Sort
         setNativeObject(Native.mkListSort(ctx.nCtx(), name.getNativeObject(),
                 elemSort.getNativeObject(), inil, iisnil, icons, iiscons, ihead,
                 itail));
-        nilDecl = new FuncDecl(ctx, inil.value);
-        isNilDecl = new FuncDecl(ctx, iisnil.value);
-        consDecl = new FuncDecl(ctx, icons.value);
-        isConsDecl = new FuncDecl(ctx, iiscons.value);
-        headDecl = new FuncDecl(ctx, ihead.value);
-        tailDecl = new FuncDecl(ctx, itail.value);
-        nilConst = ctx.mkConst(nilDecl);
     }
 };

src/ast/ast_list.h

@@ -1,160 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    ast_list.h
-
-Abstract:
-
-    Quick hack to have lists of ASTs.
-    The lists have hash-consing.
-    This is a substitute for the old expr_lists implemented on top of the ASTs.
-    The new lists live in a different manager and do not affect the ast_manager.
-
-Author:
-
-    Leonardo de Moura (leonardo) 2011-01-06.
-
-Revision History:
-
---*/
-#ifndef _AST_LIST_H_
-#define _AST_LIST_H_
-
-#include"ast.h"
-
-template<typename AST>
-class ast_list_manager_tpl;
-
-template<typename AST>
-class ast_list_tpl {
-public:
-    typedef ast_list_tpl  list;
-private:
-    unsigned m_id;
-    unsigned m_is_nil:1;
-    unsigned m_ref_count:31;
-    AST  *   m_head;
-    list *   m_tail;
-
-    ast_list_tpl():
-        m_is_nil(true),
-        m_ref_count(0),
-        m_head(0),
-        m_tail(0) {
-    }
-
-    ast_list_tpl(AST * h, list * t):
-        m_is_nil(false),
-        m_ref_count(0),
-        m_head(h),
-        m_tail(t) {
-    }
-
-    friend class ast_list_manager_tpl<AST>;
-
-    struct hash_proc;
-    friend struct hash_proc;
-    
-    struct hash_proc {
-        unsigned operator()(ast_list_tpl * l) const {
-            unsigned h1 = l->m_head ? l->m_head->get_id() : 5;
-            unsigned h2 = l->m_tail ? l->m_tail->get_id() : 7;
-            return hash_u_u(h1, h2);
-        }
-    };
-
-    struct eq_proc;
-    friend struct eq_proc;
-
-    struct eq_proc {
-        bool operator()(ast_list_tpl * l1, ast_list_tpl * l2) const {
-            return l1->m_head == l2->m_head && l1->m_tail == l2->m_tail; 
-        }
-    };
-
-    typedef ptr_hashtable<list, hash_proc, eq_proc> table; // for hash consing
-
-public:
-    unsigned get_id() const { return m_id; }
-    unsigned get_ref_count() const { return m_ref_count; }
-    unsigned hash() const { return m_id; }
-
-    friend inline bool is_nil(list const * l) { return l->m_is_nil == true; }
-    friend inline bool is_cons(list const * l) { return !is_nil(l); }
-    friend inline AST * head(list const * l) { SASSERT(is_cons(l)); return l->m_head; }
-    friend inline list * tail(list const * l) { SASSERT(is_cons(l)); return l->m_tail; }
-};
-
-template<typename AST>
-class ast_list_manager_tpl {
-public:
-    typedef ast_list_tpl<AST>   list;
-    typedef obj_hashtable<list> list_set;
-private:
-    typedef typename list::table table;
-    ast_manager &          m_manager;
-    small_object_allocator m_allocator;
-    table                  m_table;
-    id_gen                 m_id_gen;
-    list                   m_nil;
-
-public:    
-    ast_list_manager_tpl(ast_manager & m):
-        m_manager(m),
-        m_nil() {
-        m_nil.m_id = m_id_gen.mk();
-        m_nil.m_ref_count = 1;
-    }
-
-    void inc_ref(list * l) {
-        if (l != 0) {
-            l->m_ref_count++;
-        }
-    }
-
-    void dec_ref(list * l) {
-        while (l != 0) {
-            SASSERT(l->m_ref_count > 0);
-            l->m_ref_count--;
-            if (l->m_ref_count > 0) 
-                return;
-            SASSERT(l != &m_nil);
-            m_table.erase(l);
-            m_manager.dec_ref(l->m_head);
-            m_id_gen.recycle(l->m_id);
-            list * old_l = l;
-            l = l->m_tail;
-            m_allocator.deallocate(sizeof(list), old_l);
-        }
-    }
-
-    list * mk_nil() { return &m_nil; }
-
-    list * mk_cons(AST * h, list * l) {
-        list tmp(h, l);
-        list * r = 0;
-        if (m_table.find(&tmp, r)) 
-            return r;
-        r = new (m_allocator.allocate(sizeof(list))) list(h, l);
-        m_manager.inc_ref(h);
-        inc_ref(l);
-        r->m_id = m_id_gen.mk();
-        m_table.insert(r);
-        return r;
-    }
-};
-
-typedef ast_list_tpl<expr>         expr_list;
-typedef ast_list_manager_tpl<expr> expr_list_manager;
-
-typedef ast_list_tpl<quantifier>         quantifier_list;
-typedef ast_list_manager_tpl<quantifier> quantifier_list_manager;
-
-typedef obj_ref<expr_list, expr_list_manager> expr_list_ref;
-typedef obj_ref<quantifier_list, quantifier_list_manager> quantifier_list_ref;
-typedef ref_vector<expr_list, expr_list_manager> expr_list_ref_vector;
-typedef ref_vector<quantifier_list, quantifier_list_manager> quantifier_list_ref_vector;
-
-#endif

src/ast/rewriter/arith_rewriter.cpp

@@ -981,14 +981,6 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {
         result = m_util.mk_numeral(a, false);
         return BR_DONE;
     }
-#if 0
-    // The following rewriting rule is not correct.
-    // It is used only for making experiments.
-    if (m_util.is_to_int(arg)) {
-        result = to_app(arg)->get_arg(0);
-        return BR_DONE;
-    }
-#endif
     // push to_real over OP_ADD, OP_MUL
     if (m_push_to_real) {
         if (m_util.is_add(arg) || m_util.is_mul(arg)) {

src/cmd_context/echo_tactic.cpp

@@ -34,9 +34,9 @@ public:
                             expr_dependency_ref & core) {
         #pragma omp critical (echo_tactic)
         {
-            m_ctx.diagnostic_stream() << m_msg;
+            m_ctx.regular_stream() << m_msg;
             if (m_newline)
-                m_ctx.diagnostic_stream() << std::endl;
+                m_ctx.regular_stream() << std::endl;
         }
         skip_tactic::operator()(in, result, mc, pc, core);
     }

src/muz_qe/heap_trie.h

@@ -88,7 +88,7 @@ class heap_trie {
             out << " value: " << m_value;
         }
         virtual unsigned num_nodes() const { return 1; }
-        virtual unsigned num_leaves() const { return ref_count()>0?1:0; }
+        virtual unsigned num_leaves() const { return this->ref_count()>0?1:0; }
     };
 
     typedef buffer<std::pair<Key,node*>, true, 2> children_t;

src/shell/resource.h

@@ -1,14 +0,0 @@
-//{{NO_DEPENDENCIES}}
-// Microsoft Visual C++ generated include file.
-// Used by shell.rc
-
-// Next default values for new objects
-// 
-#ifdef APSTUDIO_INVOKED
-#ifndef APSTUDIO_READONLY_SYMBOLS
-#define _APS_NEXT_RESOURCE_VALUE        101
-#define _APS_NEXT_COMMAND_VALUE         40001
-#define _APS_NEXT_CONTROL_VALUE         1001
-#define _APS_NEXT_SYMED_VALUE           101
-#endif
-#endif

src/tactic/arith/probe_arith.cpp

@@ -313,23 +313,28 @@ struct is_non_nira_functor {
     bool          m_int;
     bool          m_real;
     bool          m_quant;
+    bool          m_linear;
 
-    is_non_nira_functor(ast_manager & _m, bool _int, bool _real, bool _quant):m(_m), u(m), m_int(_int), m_real(_real), m_quant(_quant) {}
+    is_non_nira_functor(ast_manager & _m, bool _int, bool _real, bool _quant, bool linear):m(_m), u(m), m_int(_int), m_real(_real), m_quant(_quant), m_linear(linear) {}
+
+    void throw_found() {
+        throw found();
+    }
 
     void operator()(var * x) {
         if (!m_quant)
-            throw found();
+            throw_found();
         sort * s = x->get_sort();
         if (m_int && u.is_int(s))
             return;
         if (m_real && u.is_real(s))
             return;
-        throw found();
+        throw_found();
     }
     
     void operator()(quantifier *) { 
         if (!m_quant)
-            throw found(); 
+            throw_found(); 
     }
     
     bool compatible_sort(app * n) const {
@@ -344,35 +349,92 @@ struct is_non_nira_functor {
 
     void operator()(app * n) {
         if (!compatible_sort(n))
-            throw found();
+            throw_found();
         family_id fid = n->get_family_id();
         if (fid == m.get_basic_family_id())
             return; 
-        if (fid == u.get_family_id())
+        if (fid == u.get_family_id()) {
+            switch (n->get_decl_kind()) {
+            case OP_LE:  case OP_GE: case OP_LT: case OP_GT:
+            case OP_ADD: case OP_UMINUS: case OP_SUB: case OP_ABS: 
+            case OP_NUM:
                 return;
+            case OP_MUL:
+                if (m_linear) {
+                    if (n->get_num_args() != 2)
+                        throw_found();
+                    if (!u.is_numeral(n->get_arg(0)))
+                        throw_found();
+                }
+                return;
+            case OP_IDIV: case OP_DIV: case OP_REM: case OP_MOD:
+                if (m_linear && !u.is_numeral(n->get_arg(1)))
+                    throw_found();
+                return;
+            case OP_IS_INT:
+                if (m_real)
+                    throw_found();
+                return;
+            case OP_TO_INT:
+            case OP_TO_REAL:
+                return;
+            case OP_POWER:
+                if (m_linear)
+                    throw_found();
+                return;
+            case OP_IRRATIONAL_ALGEBRAIC_NUM:
+                if (m_linear || !m_real)
+                    throw_found();
+                return;
+            default:
+                throw_found();
+            }
+            return;
+        }
+
         if (is_uninterp_const(n))
             return;
-        throw found();
+        throw_found();
     }
 };
 
 static bool is_qfnia(goal const & g) {
-    is_non_nira_functor p(g.m(), true, false, false);
+    is_non_nira_functor p(g.m(), true, false, false, false);
     return !test(g, p);
 }
 
 static bool is_qfnra(goal const & g) {
-    is_non_nira_functor p(g.m(), false, true, false);
+    is_non_nira_functor p(g.m(), false, true, false, false);
     return !test(g, p);
 }
 
 static bool is_nia(goal const & g) {
-    is_non_nira_functor p(g.m(), true, false, true);
+    is_non_nira_functor p(g.m(), true, false, true, false);
     return !test(g, p);
 }
 
 static bool is_nra(goal const & g) {
-    is_non_nira_functor p(g.m(), false, true, true);
+    is_non_nira_functor p(g.m(), false, true, true, false);
+    return !test(g, p);
+}
+
+static bool is_nira(goal const & g) {
+    is_non_nira_functor p(g.m(), true, true, true, false);
+    return !test(g, p);
+}
+
+static bool is_lra(goal const & g) {
+    is_non_nira_functor p(g.m(), false, true, true, true);
+    return !test(g, p);
+}
+
+static bool is_lia(goal const & g) {
+    is_non_nira_functor p(g.m(), true, false, true, true);
+    return !test(g, p);
+}
+
+static bool is_lira(goal const & g) {
+    is_non_nira_functor p(g.m(), true, true, true, true);
     return !test(g, p);
 }
 
@@ -404,6 +466,34 @@ public:
     }
 };
 
+class is_nira_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_nira(g);
+    }
+};
+
+class is_lia_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_lia(g);
+    }
+};
+
+class is_lra_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_lra(g);
+    }
+};
+
+class is_lira_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return is_lira(g);
+    }
+};
+
 probe * mk_is_qfnia_probe() {
     return alloc(is_qfnia_probe);
 }
@@ -419,3 +509,19 @@ probe * mk_is_nia_probe() {
 probe * mk_is_nra_probe() {
     return alloc(is_nra_probe);
 }
+
+probe * mk_is_nira_probe() {
+    return alloc(is_nira_probe);
+}
+
+probe * mk_is_lia_probe() {
+    return alloc(is_lia_probe);
+}
+
+probe * mk_is_lra_probe() {
+    return alloc(is_lra_probe);
+}
+
+probe * mk_is_lira_probe() {
+    return alloc(is_lira_probe);
+}

src/tactic/arith/probe_arith.h

@@ -49,11 +49,19 @@ probe * mk_is_qfnia_probe();
 probe * mk_is_qfnra_probe();
 probe * mk_is_nia_probe();
 probe * mk_is_nra_probe();
+probe * mk_is_nira_probe();
+probe * mk_is_lia_probe();
+probe * mk_is_lra_probe();
+probe * mk_is_lira_probe();
 
 /*
   ADD_PROBE("is-qfnia", "true if the goal is in QF_NIA (quantifier-free nonlinear integer arithmetic).", "mk_is_qfnia_probe()")
   ADD_PROBE("is-qfnra", "true if the goal is in QF_NRA (quantifier-free nonlinear real arithmetic).", "mk_is_qfnra_probe()")
   ADD_PROBE("is-nia", "true if the goal is in NIA (nonlinear integer arithmetic, formula may have quantifiers).", "mk_is_nia_probe()")
   ADD_PROBE("is-nra", "true if the goal is in NRA (nonlinear real arithmetic, formula may have quantifiers).", "mk_is_nra_probe()")
+  ADD_PROBE("is-nira", "true if the goal is in NIRA (nonlinear integer and real arithmetic, formula may have quantifiers).", "mk_is_nira_probe()")
+  ADD_PROBE("is-lia", "true if the goal is in LIA (linear integer arithmetic, formula may have quantifiers).", "mk_is_lia_probe()")
+  ADD_PROBE("is-lra", "true if the goal is in LRA (linear real arithmetic, formula may have quantifiers).", "mk_is_lra_probe()")
+  ADD_PROBE("is-lira", "true if the goal is in LIRA (linear integer and real arithmetic, formula may have quantifiers).", "mk_is_lira_probe()")
 */
 #endif

src/tactic/goal.cpp

@@ -111,19 +111,29 @@ void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
     if (m().is_true(f))
         return;
     if (m().is_false(f)) {
+        // Make sure pr and d are not deleted by the m().del(...) statements.
+        proof_ref saved_pr(m());
+        expr_dependency_ref saved_d(m());
+        saved_pr = pr;
+        saved_d  = d;
         m().del(m_forms);
         m().del(m_proofs);
         m().del(m_dependencies);
         m_inconsistent = true;
+        m().push_back(m_forms, m().mk_false());
+        if (proofs_enabled())
+            m().push_back(m_proofs, saved_pr);
+        if (unsat_core_enabled())
+            m().push_back(m_dependencies, saved_d);
     }
     else {
         SASSERT(!m_inconsistent);
-    }
         m().push_back(m_forms, f);
         if (proofs_enabled())
             m().push_back(m_proofs, pr);
         if (unsat_core_enabled())
             m().push_back(m_dependencies, d);
+    }
 }
 
 void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {

src/tactic/portfolio/default_tactic.cpp

@@ -26,22 +26,18 @@ Notes:
 #include"qfnra_tactic.h"
 #include"nra_tactic.h"
 #include"probe_arith.h"
+#include"quant_tactics.h"
 
 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(),
+                                        cond(mk_is_qfbv_probe(),  mk_qfbv_tactic(m),
-                                             mk_qfbv_tactic(m),
+                                        cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
-                                             cond(mk_is_qflia_probe(),
+                                        cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
-                                                  mk_qflia_tactic(m),
+                                        cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),
-                                                  cond(mk_is_qflra_probe(),
+                                        cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),
-                                                       mk_qflra_tactic(m),
+                                        cond(mk_is_nra_probe(),   mk_nra_tactic(m),
-                                                       cond(mk_is_qfnra_probe(),
+                                        cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
-                                                            mk_qfnra_tactic(m),
+                                             mk_smt_tactic())))))))),
-                                                            cond(mk_is_qfnia_probe(),
-                                                                 mk_qfnia_tactic(m),
-                                                                 cond(mk_is_nra_probe(),
-                                                                      mk_nra_tactic(m),
-                                                                      mk_smt_tactic()))))))),
                                p);
     return st;
 }

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -72,6 +72,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
         return mk_uflra_tactic(m, p);
     else if (logic=="LRA")
         return mk_lra_tactic(m, p);
+    else if (logic=="LIA")
+        return mk_lia_tactic(m, p);
     else if (logic=="UFBV")
         return mk_ufbv_tactic(m, p);
     else if (logic=="BV")

src/tactic/smtlogics/quant_tactics.cpp

@@ -104,3 +104,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
     return st;
 }
 
+tactic * mk_lia_tactic(ast_manager & m, params_ref const & p) {
+    return mk_lra_tactic(m, p);
+}
+
+tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) {
+    return mk_lra_tactic(m, p);
+}

src/tactic/smtlogics/quant_tactics.h

@@ -29,5 +29,7 @@ tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
+tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
+tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
 
 #endif