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

.gitignore

@@ -64,3 +64,6 @@ src/util/version.h
 src/api/java/Native.cpp
 src/api/java/Native.java
 src/api/java/enumerations/*.java
+*.bak
+doc/api
+doc/code

RELEASE_NOTES

@@ -1,8 +1,22 @@
 RELEASE NOTES
 
+Version 4.3.3
+=============
+
+- Fixed bug in floating point models
+
 Version 4.3.2
 =============
 
+- Added preliminary support for the theory of floating point numbers (tactics qffpa, qffpabv, and logics QF_FPA, QF_FPABV).
+
+- Added the interpolation features of iZ3, which are now integrated into the Z3. 
+
+- Fixed a multitude of bugs and inconsistencies that were reported to us either in person, by email, or on Codeplex. Of those that we do have records of, we would like to express our gratitude to:
+    Vladimir Klebanov, Konrad Jamrozik, Nuno Lopes, Carsten Ruetz, Esteban Pavese, Tomer Weiss, Ilya Mironov, Gabriele Paganelli, Levent Erkok, Fabian Emmes, David Cok, Etienne Kneuss, Arlen Cox, Matt Lewis, Carsten Otto, Paul Jackson, David Monniaux, Markus Rabe, Martin Pluecker, Jasmin Blanchette, Jules Villard, Andrew Gacek, George Karpenkov, Joerg Pfaehler, and Pablo Aledo
+    as well as the following Codeplex users that either reported bugs or took part in discussions:
+xor88, parno, gario, Bauna, GManNickG, hanwentao, dinu09, fhowar, Cici, chinissai, barak_cohen, tvalentyn, krikunts, sukyoung, daramos, snedunuri, rajtendulkar, sonertari, nick8325, dvitek, amdragon, Beatgodes, dmonniaux, nickolai, DameNingen, mangpo, ttsiodras, blurium, sbrickey, pcodemod, indranilsaha, apanda, hougaardj, yoff, EfForEffort, Ansotegui, scottgw, viorelpreoteasa, idudka, c2855337, gario, jnfoster, omarmrivas, switicus, vosandi, foens, yzwwf, Heizmann, znajem, ilyagri, hougaardj, cliguda, rgrig, 92c849c1ccc707173, edmcman, cipher1024, MichaelvW, hellok, n00b42, ic3guy, Adorf, tvcsantos, zilongwang, Elarnon, immspw, jbridge99, danliew, zverlov, petross, jmh93, dradorf, fniksic, Heyji, cxcfan, henningg, wxlfrank, rvprasad, MovGP0, jackie1015, cowang, ffaghih, sanpra1989, gzchenyin, baitman, xjtulixiangyang, andreis, trucnguyenlam, erizzi, hanhchi, qsp, windypan, vadave, gradanne, SamWot, gsingh93, manjeetdahiya, zverlov, RaLa, and regehr.
+
 - New parameter setting infrastructure. Now, it is possible to set parameter for Z3 internal modules. Several parameter names changed. Execute `z3 -p` for the new parameter list.
 
 - Added get_version() and get_version_string() to Z3Py

doc/mk_api_doc.py

@@ -27,6 +27,10 @@ try:
     shutil.copyfile('website.dox', 'tmp/website.dox')
     shutil.copyfile('../src/api/python/z3.py', 'tmp/z3py.py')
     cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h')
+    cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h')
+    cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h')
+    cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h')
+    cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
     
     print "Removed annotations from z3_api.h."
     try:
@@ -38,6 +42,10 @@ try:
         exit(1)
     print "Generated C and .NET API documentation."
     os.remove('tmp/z3_api.h')
+    os.remove('tmp/z3_algebraic.h')
+    os.remove('tmp/z3_polynomial.h')
+    os.remove('tmp/z3_rcf.h')
+    os.remove('tmp/z3_interp.h')
     print "Removed temporary file z3_api.h."
     os.remove('tmp/website.dox')	
     print "Removed temporary file website.dox"

doc/website.dox

@@ -15,5 +15,5 @@
    - <a class="el" href="class_microsoft_1_1_z3_1_1_context.html">.NET API</a>
    - <a class="el" href="namespacecom_1_1microsoft_1_1z3.html">Java API</a>
    - <a class="el" href="namespacez3py.html">Python API</a> (also available in <a class="el" href="z3.html">pydoc format</a>).
-   - Try Z3 online at <a href="http://rise4fun.com/z3py">RiSE4Fun</a> using <a href="http://rise4fun.com/z3py">Python</a> or <a href="http://rise4fun.com/z3">SMT 2.0</a>.
+   - Try Z3 online at <a href="http://rise4fun.com/z3">RiSE4Fun</a>.
 */

doc/z3api.dox

@@ -363,7 +363,7 @@ TYPEDEF_HIDES_STRUCT   = NO
 # 2^(16+SYMBOL_CACHE_SIZE). The valid range is 0..9, the default is 0,
 # corresponding to a cache size of 2^16 = 65536 symbols.
 
-SYMBOL_CACHE_SIZE      = 0
+# SYMBOL_CACHE_SIZE      = 0
 
 # Similar to the SYMBOL_CACHE_SIZE the size of the symbol lookup cache can be
 # set using LOOKUP_CACHE_SIZE. This cache is used to resolve symbols given
@@ -708,7 +708,11 @@ INPUT_ENCODING         = UTF-8
 # *.f90 *.f *.for *.vhd *.vhdl
 
 FILE_PATTERNS          = website.dox \
-                         z3_api.h \
+			 z3_api.h \
+			 z3_algebraic.h \
+			 z3_polynomial.h \
+			 z3_rcf.h \
+			 z3_interp.h \
                          z3++.h \
                          z3py.py \
                          ApplyResult.cs \
@@ -1477,13 +1481,13 @@ XML_OUTPUT             = xml
 # which can be used by a validating XML parser to check the
 # syntax of the XML files.
 
-XML_SCHEMA             =
+# XML_SCHEMA             =
 
 # The XML_DTD tag can be used to specify an XML DTD,
 # which can be used by a validating XML parser to check the
 # syntax of the XML files.
 
-XML_DTD                =
+# XML_DTD                =
 
 # If the XML_PROGRAMLISTING tag is set to YES Doxygen will
 # dump the program listings (including syntax highlighting
@@ -1699,7 +1703,7 @@ DOT_NUM_THREADS        = 0
 # the DOTFONTPATH environment variable or by setting DOT_FONTPATH to the
 # directory containing the font.
 
-DOT_FONTNAME           = FreeSans
+# DOT_FONTNAME           = FreeSans
 
 # The DOT_FONTSIZE tag can be used to set the size of the font of dot graphs.
 # The default size is 10pt.

examples/java/README

@@ -1,7 +1,6 @@
-### This is work-in-progress and does not work yet.
+A small example using the Z3 Java bindings.   
 
-Small example using the Z3 Java bindings.
+To build the example, configure Z3 with the --java option to scripts/mk_make.py, build via  
-To build the example execute
    make examples
 in the build directory.
 
@@ -11,5 +10,5 @@ which can be run on Windows via
 
 On Linux and FreeBSD, we must use
    LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample
- 
+On OSX, the corresponding option is DYLD_LIBRARY_PATH:   
-   
+   DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample  

scripts/mk_project.py

@@ -9,7 +9,7 @@ from mk_util import *
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 3, 2, 0)
+    set_version(4, 3, 3, 0)
     add_lib('util', [])
     add_lib('polynomial', ['util'], 'math/polynomial')
     add_lib('sat', ['util'])

scripts/update_api.py

@@ -297,11 +297,13 @@ def param2javaw(p):
     k = param_kind(p)
     if k == OUT:
         return "jobject"
-    if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
+    elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
         if param_type(p) == INT or param_type(p) == UINT:
             return "jintArray"
         else:
             return "jlongArray"
+    elif k == OUT_MANAGED_ARRAY:
+        return "jlong";
     else:
         return type2javaw(param_type(p))
 

src/api/api_interp.cpp

@@ -273,6 +273,9 @@ extern "C" {
                                        0 // ignore params for now
                                        );
 
+        for (unsigned i = 0; i < cnsts.size(); i++)
+            _m.dec_ref(cnsts[i]);
+
         Z3_lbool status = of_lbool(_status);
 
         Z3_ast_vector_ref *v = 0;
@@ -617,7 +620,7 @@ extern "C" {
         }
 
         for (unsigned j = 0; j < num - 1; j++)
-            if (read_parents[j] == SHRT_MIN){
+            if (read_parents[j] == SHRT_MAX){
             read_error << "formula " << j + 1 << ": unreferenced";
             goto fail;
             }
@@ -717,4 +720,4 @@ Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
                                __in unsigned incremental,
                                __in unsigned num_theory,
                                __in_ecount(num_theory) Z3_ast *theory);
-#endif
+#endif

src/api/dotnet/Properties/AssemblyInfo

@@ -12,7 +12,7 @@ using System.Security.Permissions;
 [assembly: AssemblyConfiguration("")]
 [assembly: AssemblyCompany("Microsoft Corporation")]
 [assembly: AssemblyProduct("Z3")]
-[assembly: AssemblyCopyright("Copyright © Microsoft Corporation 2006")]
+[assembly: AssemblyCopyright("Copyright (C) 2006-2014 Microsoft Corporation")]
 [assembly: AssemblyTrademark("")]
 [assembly: AssemblyCulture("")]
 

src/api/java/AST.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from AST.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    AST.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
@@ -13,28 +24,12 @@ import com.microsoft.z3.enumerations.Z3_ast_kind;
  **/
 public class AST extends Z3Object
 {
-    /**
-     * Comparison operator. <param name="a">An AST</param> <param name="b">An
-     * AST</param>
-     * 
-     * @return True if <paramref name="a"/> and <paramref name="b"/> are from
-     *         the same context and represent the same sort; false otherwise.
-     **/
-    /* Overloaded operators are not translated. */
-
-    /**
-     * Comparison operator. <param name="a">An AST</param> <param name="b">An
-     * AST</param>
-     * 
-     * @return True if <paramref name="a"/> and <paramref name="b"/> are not
-     *         from the same context or represent different sorts; false
-     *         otherwise.
-     **/
     /* Overloaded operators are not translated. */
 
     /**
      * Object comparison.
-     **/
+     * <param name="o">another AST</param>
+     **/    
     public boolean equals(Object o)
     {
         AST casted = null;

src/api/java/ASTDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    ASTDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ASTMap.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ASTMap.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ASTMap.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ASTVector.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ASTVector.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ASTVector.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/AlgebraicNum.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from AlgebraicNum.cs
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter) 
+Module Name:
- **/
+
+    AlgebraicNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ApplyResult.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ApplyResult.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ApplyResult.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ApplyResultDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    ApplyResultDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ArithExpr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArithExpr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- * **/
+
+    ArithExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ArithSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArithSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ArithSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ArrayExpr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArrayExpr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ArrayExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ArraySort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ArraySort.cs
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter) 
+Module Name:
- **/
+
+    ArraySort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/AstMapDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    AstMapDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/AstVectorDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    AstVectorDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/BitVecExpr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BitVecExpr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    BitVecExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/BitVecNum.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BitVecNum.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    BitVecNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/BitVecSort.java

@@ -1,8 +1,20 @@
 /**
- * This file was automatically generated from BitVecSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    BitVecSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
+
 package com.microsoft.z3;
 
 /**

src/api/java/BoolExpr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BoolExpr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    BoolExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/BoolSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from BoolSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    BoolSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/Constructor.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Constructor.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Constructor.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/ConstructorList.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ConstructorList.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ConstructorList.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/Context.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Context.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Context.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/DatatypeExpr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from DatatypeExpr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    DatatypeExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/DatatypeSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from DatatypeSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    DatatypeSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/EnumSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from EnumSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    EnumSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/Expr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Expr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Expr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 
@@ -29,7 +40,7 @@ public class Expr extends AST
 	/**
 	 * Returns a simplified version of the expression 
 	 * A set of
-	 * parameters <param name="p" /> to configure the simplifier 
+	 * parameters <param name="p">a Params object</param> to configure the simplifier 
 	 * <seealso cref="Context.SimplifyHelp"/>
 	 **/
 	public Expr simplify(Params p) throws Z3Exception

src/api/java/FiniteDomainSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from FiniteDomainSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    FiniteDomainSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/Fixedpoint.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Fixedpoint.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Fixedpoint.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/FixedpointDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    FixedpointDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/FuncDecl.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from FuncDecl.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    FuncDecl.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/FuncInterp.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from FuncInterp.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    FuncInterp.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/FuncInterpDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    FuncInterpDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/FuncInterpEntryDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    FuncInterpEntryDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/Global.java

@@ -1,7 +1,19 @@
 /**
- * Global.java
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    Global.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
@@ -38,8 +50,7 @@ public final class Global
     /**
      * Get a global (or module) parameter.     
      * <remarks>               
-     * Returns null if the parameter <param name="id"/> does not exist.
+     * Returns null if the parameter <param name="id">parameter id</param> does not exist.     
-     * The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
      * This function cannot be invoked simultaneously from different threads without synchronization.
      * The result string stored in param_value is stored in a shared location.
      * </remarks>
@@ -58,7 +69,7 @@ public final class Global
      * <remarks>
      * This command will not affect already created objects (such as tactics and solvers)
      * </remarks>
-     * @seealso SetParameter
+     * <seealso cref="SetParameter"/>
      **/
     public static void resetParameters()
     {

src/api/java/Goal.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Goal.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Goal.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/GoalDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    GoalDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/IDecRefQueue.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IDecRefQueue.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    IDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/
 
 package com.microsoft.z3;
 

src/api/java/IntExpr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntExpr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    IntExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/IntNum.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntNum.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    IntNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/IntSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    IntSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/IntSymbol.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from IntSymbol.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    IntSymbol.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/InterpolationContext.java

@@ -1,6 +1,20 @@
 /**
- * 
+Copyright (c) 2012-2014 Microsoft Corporation
- */
+   
+Module Name:
+
+   InterpolationContext.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
 package com.microsoft.z3;
 
 import java.util.Map;

src/api/java/ListSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ListSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ListSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Log.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Log.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Log.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Model.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Model.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Model.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/ModelDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    ModelDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/ParamDescrs.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from ParamDescrs.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    ParamDescrs.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/ParamDescrsDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    ParamDescrsDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Params.java

@@ -1,8 +1,20 @@
 /**
- * This file was automatically generated from Params.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Params.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
+
 
 package com.microsoft.z3;
 

src/api/java/ParamsDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    ParamDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Pattern.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Pattern.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Pattern.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Probe.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Probe.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Probe.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/ProbeDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    ProbeDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Quantifier.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Quantifier.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Quantifier.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/README

@@ -1,3 +1,6 @@
 Java bindings
 -------------
 
+The Java bindings will be included in the Z3 build if it is configured with   
+the option --java to python scripts/mk_make.py. This will produce the   
+com.microsoft.z3.jar package in the build directory.

src/api/java/RatNum.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RatNum.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    RatNum.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/RealExpr.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RealExpr.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    RealExpr.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/RealSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RealSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    RealSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/RelationSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from RelationSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    RelationSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/SetSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from SetSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    SetSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Solver.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Solver.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Solver.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/SolverDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    SolverDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Sort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Sort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Sort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 
@@ -14,27 +25,10 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
  **/
 public class Sort extends AST
 {
-    /**
-     * Comparison operator. <param name="a">A Sort</param> <param name="b">A
-     * Sort</param>
-     * 
-     * @return True if <paramref name="a"/> and <paramref name="b"/> are from
-     *         the same context and represent the same sort; false otherwise.
-     **/
     /* Overloaded operators are not translated. */
 
     /**
-     * Comparison operator. <param name="a">A Sort</param> <param name="b">A
+     * Equality operator for objects of type Sort. <param name="o"/>
-     * Sort</param>
-     * 
-     * @return True if <paramref name="a"/> and <paramref name="b"/> are not
-     *         from the same context or represent different sorts; false
-     *         otherwise.
-     **/
-    /* Overloaded operators are not translated. */
-
-    /**
-     * Equality operator for objects of type Sort. <param name="o"></param>
      * 
      * @return
      **/

src/api/java/Statistics.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Statistics.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Statistics.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/StatisticsDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    StatisticsDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Status.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Status.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Status.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/StringSymbol.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from StringSymbol.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    StringSymbol.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Symbol.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Symbol.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Symbol.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Tactic.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Tactic.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Tactic.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/TacticDecRefQueue.java

@@ -1,7 +1,19 @@
 /**
- * Copyright (c) 2012 Microsoft Corporation
+Copyright (c) 2012-2014 Microsoft Corporation
- * @author Christoph M. Wintersteiger (cwinter)
+   
- **/
+Module Name:
+
+    TacticDecRefQueue.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/TupleSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from TupleSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    TupleSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/UninterpretedSort.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from UninterpretedSort.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    UninterpretedSort.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Version.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Version.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Version.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Z3Exception.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Z3Exception.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Z3Exception.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/Z3Object.java

@@ -1,8 +1,19 @@
 /**
- * This file was automatically generated from Z3Object.cs 
+Copyright (c) 2012-2014 Microsoft Corporation
- * w/ further modifications by:
+   
- * @author Christoph M. Wintersteiger (cwinter)
+Module Name:
- **/
+
+    Z3Object.java
+
+Abstract:
+
+Author:
+
+    @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+    
+**/ 
 
 package com.microsoft.z3;
 

src/api/java/manifest

@@ -1,2 +1,2 @@
 Manifest-Version: 1.0
-Created-By: 4.3.0 (Microsoft Research LTD.)
+Created-By: 4.3.2 (Microsoft Research LTD.)

src/api/java/mk_java.py

@@ -1,463 +0,0 @@
-######################################################
-# Copyright (c) 2012 Microsoft Corporation
-# 
-# Auxiliary scripts for generating Java bindings
-# from the managed API.
-#
-# Author: Christoph M. Wintersteiger (cwinter)
-######################################################
-
-
-###
-# DO NOT USE THIS SCRIPT! 
-# This script creates a rough draft of a Java API from
-# the managed API, but does not automated the process.
-###
-
-CS="../dotnet/"
-EXT=".cs"
-EXCLUDE=["Enumerations.cs", "Native.cs", "AssemblyInfo.cs"]
-OUTDIR="com/Microsoft/Z3/"
-ENUMS_FILE = "Enumerations.cs"
-
-import os
-import fileinput
-import string
-import re
-
-EXCLUDE_METHODS = [ [ "Context.cs", "public Expr MkNumeral(ulong" ],
-                    [ "Context.cs", "public Expr MkNumeral(uint" ],
-                    [ "Context.cs", "public RatNum MkReal(ulong" ],
-                    [ "Context.cs", "public RatNum MkReal(uint" ],
-                    [ "Context.cs", "public IntNum MkInt(ulong" ],
-                    [ "Context.cs", "public IntNum MkInt(uint" ],
-                    [ "Context.cs", "public BitVecNum MkBV(ulong" ],
-                    [ "Context.cs", "public BitVecNum MkBV(uint" ],
-                    ]
-
-ENUMS = []
-
-def mk_java_bindings():
-    print "Generating Java bindings (from C# bindings in " + CS + ")..."
-    print "Finding enumerations in " + ENUMS_FILE + "..."
-    find_enums(ENUMS_FILE)
-    for root, dirs, files in os.walk(CS):
-        for fn in files:
-            if not fn in EXCLUDE and fn.endswith(EXT):
-                translate(fn)
-
-def subst_getters(s, getters):
-    for g in getters:
-        s = s.replace(g, g + "()")
-
-def type_replace(s):
-    s = s.replace(" bool", " boolean")
-    s = s.replace("(bool", "(boolean")
-    s = s.replace("uint", "int")
-    s = s.replace("ulong", "long")
-    s = s.replace("string", "String")
-    s = s.replace("IntPtr", "long")
-    s = s.replace("Dictionary<", "Map<")
-    s = s.replace("UInt64", "long")
-    s = s.replace("Int64", "long")
-    s = s.replace("List<long>", "LinkedList<Long>")
-    s = s.replace("System.Exception", "Exception")
-    return s
-
-def rename_native(s):
-    while s.find("Native.Z3") != -1:
-        i0 = s.find("Native.Z3")
-        i1 = s.find("(", i0)
-        c0 = s[:i0]
-        c1 = s[i0:i1]
-        c1 = c1.replace("Native.Z3_", "Native.")
-        c2 = s[i1:]
-        lc_callback = lambda pat: pat.group("id").upper()
-        c1 = re.sub("_(?P<id>\w)", lc_callback, c1)
-        s = c0 + c1 + c2
-    return s
-
-def find_enums(fn):
-    for line in fileinput.input(os.path.join(CS, fn)):
-        s = string.rstrip(string.lstrip(line))
-        if s.startswith("public enum"):
-            ENUMS.append(s.split(" ")[2])
-
-
-def enum_replace(line):
-    for e in ENUMS:
-        if line.find("case") != -1:
-            line = line.replace(e + ".", "")
-        elif line.find("== (int)") != -1 or line.find("!= (int)") != -1:
-            line = re.sub("\(int\)" + e + "\.(?P<id>[A-Z0-9_]*)", e + ".\g<id>.toInt()", line)
-        elif line.find("==") != -1 or line.find("!=") != -1:
-            line = re.sub(e + "\.(?P<id>[A-Z0-9_]*)", e + ".\g<id>", line)
-        else:
-            # line = re.sub("\(\(" + e + "\)(?P<rest>.*\(.*)\)", "(" + e + ".values()[\g<rest>])", line)
-            line = re.sub("\(" + e + "\)(?P<rest>.*\(.*\))", e + ".fromInt(\g<rest>)", line)
-    return line
-
-def replace_generals(a):
-    a = re.sub(" NativeObject", " NativeObject()", a)
-    a = re.sub("\.NativeObject", ".NativeObject()", a)
-    a = re.sub("(?P<h>[\.\(])Id", "\g<h>Id()", a)
-    a = a.replace("(Context ==", "(Context() ==")
-    a = a.replace("(Context,", "(Context(),")
-    a = a.replace("Context.", "Context().")    
-    a = a.replace(".nCtx", ".nCtx()")    
-    a = a.replace("(nCtx", "(nCtx()")    
-    a = re.sub("Context\(\).(?P<id>[^_]*)_DRQ", "Context().\g<id>_DRQ()", a)
-    a = re.sub("ASTKind", "ASTKind()", a)
-    a = re.sub("IsExpr(?P<f>[ ;])", "IsExpr()\g<f>", a)
-    a = re.sub("IsNumeral(?P<f>[ ;])", "IsNumeral()\g<f>", a)
-    a = re.sub("IsInt(?P<f>[ ;])", "IsInt()\g<f>", a)
-    a = re.sub("IsReal(?P<f>[ ;])", "IsReal()\g<f>", a)
-    a = re.sub("IsVar(?P<f>[ ;\)])", "IsVar()\g<f>", a)
-    a = re.sub("FuncDecl.DeclKind", "FuncDecl().DeclKind()", a)
-    a = re.sub("FuncDecl.DomainSize", "FuncDecl().DomainSize()", a)
-    a = re.sub("(?P<h>[=&]) Num(?P<id>[a-zA-Z]*)", "\g<h> Num\g<id>()", a)
-    a = re.sub("= Denominator", "= Denominator()", a)
-    a = re.sub(", BoolSort(?P<f>[\)\.])", ", BoolSort()\g<f>", a)
-    a = re.sub(", RealSort(?P<f>[\)\.])", ", RealSort()\g<f>", a)
-    a = re.sub(", IntSort(?P<f>[\)\.])", ", IntSort()\g<f>", a)
-    a = a.replace("? 1 : 0", "? true : false")
-    if a.find("Native.") != -1 and a.find("!= 0") != -1:
-        a = a.replace("!= 0", "")
-    if a.find("Native.") != -1 and a.find("== 0") != -1:
-        a = a.replace("== 0", "^ true")
-    return a
-
-def translate(filename):
-    tgtfn = OUTDIR + filename.replace(EXT, ".java")
-    print "Translating " + filename + " to " + tgtfn
-    tgt = open(tgtfn, "w")
-    in_header = 0
-    in_class = 0
-    in_static_class = 0
-    in_javadoc = 0
-    lastindent = 0
-    skip_brace = 0
-    in_getter = ""
-    in_getter_type = ""
-    in_unsupported = 0
-    getters = []
-    in_bracket_op = 0
-    in_getter_get = 0
-    in_getter_set = 0
-    had_ulong_res = 0
-    in_enum = 0
-    missing_foreach_brace = 0
-    foreach_opened_brace = 0
-    for line in fileinput.input(os.path.join(CS, filename)):
-        s = string.rstrip(string.lstrip(line))
-        if in_javadoc:
-            if s.startswith("///"):
-                lastindent = line.find(s);
-                if s.startswith("/// </summary>"):
-                    pass
-                else: 
-                    a = line
-                    a = a.replace("<c>", "<code>")
-                    a = a.replace("</c>", "</code>")
-                    a = a.replace("///"," *")
-                    a = a.replace("<returns>","@return ")
-                    a = a.replace("</returns>","")
-                    tgt.write(a)
-            else:
-                t = ""
-                for i in range(0, lastindent):
-                    t += " "
-                tgt.write(t + " **/\n")
-                in_javadoc = 0
-
-        # for i in range(0, len(EXCLUDE_METHODS)):
-        #     if filename == EXCLUDE_METHODS[i][0] and s.startswith(EXCLUDE_METHODS[i][1]):
-        #         tgt.write(t + "/* Not translated because it would translate to a function with clashing types. */\n")
-        #         in_unsupported = 1
-        #         break
-                    
-
-        if in_unsupported:
-            if s == "}":
-                in_unsupported = 0                
-        elif not in_javadoc:
-            if not in_header and s.find("/*++") != -1:
-                in_header = 1
-                tgt.write("/**\n")
-            elif in_header and s.startswith("--*/"):
-                in_header = 0
-                tgt.write(" * This file was automatically generated from " + filename + " \n")
-                tgt.write(" **/\n")
-                tgt.write("\npackage com.Microsoft.Z3;\n\n")
-                tgt.write("import java.math.BigInteger;\n")
-                tgt.write("import java.util.*;\n")
-                tgt.write("import java.lang.Exception;\n")
-                tgt.write("import com.Microsoft.Z3.Enumerations.*;\n")
-            elif in_header == 1:
-                # tgt.write(" * " + line.replace(filename, tgtfn))
-                pass
-            elif s.startswith("using"):
-                if s.find("System.Diagnostics.Contracts") == -1:
-                    tgt.write("/* " + s + " */\n")
-            elif s.startswith("namespace"):
-                pass
-            elif s.startswith("public") and s.find("operator") != -1 and (s.find("==") != -1 or s.find("!=") != -1):
-                t = ""
-                for i in range(0, line.find(s)+1):
-                    t += " "                    
-                tgt.write(t + "/* Overloaded operators are not translated. */\n")
-                in_unsupported = 1
-            elif s.startswith("public enum"):
-                tgt.write(line.replace("enum", "class"))
-                in_enum = 1
-            elif in_enum == 1:
-                if s == "}":
-                    tgt.write(line)
-                    in_enum = 0
-                else:
-                    line = re.sub("(?P<id>.*)\W*=\W*(?P<val>[^\n,])", "public static final int \g<id> = \g<val>;", line)
-                    tgt.write(line.replace(",",""))
-            elif s.startswith("public class") or s.startswith("internal class") or s.startswith("internal abstract class"):
-                a = line.replace(":", "extends").replace("internal ", "")
-                a = a.replace(", IComparable", "")
-                a = type_replace(a)
-                tgt.write(a)
-                in_class = 1
-                in_static_class = 0
-            elif s.startswith("public static class") or s.startswith("abstract class"):
-                tgt.write(line.replace(":", "extends").replace("static", "final"))
-                in_class = 1
-                in_static_class = 1
-            elif s.startswith("/// <summary>"):
-                tgt.write(line.replace("/// <summary>", "/**"))
-                in_javadoc = 1
-            elif skip_brace and s == "{":
-                skip_brace = 0
-            elif ((s.find("public") != -1 or s.find("protected") != -1) and s.find("class") == -1 and s.find("event") == -1 and s.find("(") == -1) or s.startswith("internal virtual IntPtr NativeObject") or s.startswith("internal Context Context"):
-                if (s.startswith("new")):
-                    s = s[3:]
-                s = s.replace("internal virtual", "")
-                s = s.replace("internal", "")
-                tokens = s.split(" ")
-                # print "TOKENS: " + str(len(tokens))
-                if len(tokens) == 3:
-                    in_getter = tokens[2]
-                    in_getter_type = type_replace((tokens[0] + " " + tokens[1]))
-                    if in_static_class:
-                        in_getter_type = in_getter_type.replace("static", "")                        
-                    lastindent = line.find(s)
-                    skip_brace = 1
-                    getters.append(in_getter)
-                elif len(tokens) == 4:
-                    if tokens[2].startswith("this["):
-                        in_bracket_op = 1
-                        in_getter = type_replace(tokens[2]).replace("this[", "get(")
-                        in_getter += " " + tokens[3].replace("]", ")")
-                        in_getter_type = type_replace(tokens[0] + " " + tokens[1])
-                    else:
-                        in_getter = tokens[3]
-                        in_getter_type = type_replace(tokens[0] + " " + tokens[1] + " " + tokens[2])
-                    if in_static_class:
-                        in_getter_type = in_getter_type.replace("static", "")
-                    lastindent = line.find(s)
-                    skip_brace = 1         
-                    getters.append(in_getter)       
-                else:
-                    in_getter = tokens[2]
-                    in_getter_type = type_replace(tokens[0] + " " + tokens[1])
-                    if tokens[2].startswith("this["):
-                        lastindent = line.find(s)
-                        t = ""
-                        for i in range(0, lastindent): t += " "                                
-                        tgt.write(t + "/* operator this[] not translated */\n ")
-                        in_unsupported = 1
-                    else:
-                        if in_static_class:
-                            in_getter_type = in_getter_type.replace("static", "")                        
-                        rest = s[s.find("get ") + 4:-1]
-                        subst_getters(rest, getters)
-                        rest = type_replace(rest)
-                        rest = rename_native(rest)
-                        rest = replace_generals(rest)
-                        rest = enum_replace(rest)
-                        t = ""
-                        for i in range(0, lastindent):
-                            t += " "
-                        tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n")
-                        if rest.find("}") == -1:
-                            in_getter_get = 1
-                        else:
-                            getters.append(in_getter)
-                            in_getter = ""
-                        in_getter_type = ""
-                print "ACC: " + s + " --> " + in_getter
-            elif s.find("{ get {") != -1:
-                line = type_replace(line)
-                line = line.replace("internal ", "")
-                d = line[0:line.find("{ get")]
-                rest = line[line.find("{ get")+5:]
-                rest = rest.replace("} }", "}")
-                rest = re.sub("Contract.\w+\([\s\S]*\);", "", rest)
-                subst_getters(rest, getters)
-                rest = rename_native(rest)
-                rest = replace_generals(rest)
-                rest = enum_replace(rest)
-                if  in_bracket_op:
-                    tgt.write(d + rest)
-                else:
-                    tgt.write(d + "()" + rest)
-                print "ACC: " + s + " --> " + in_getter
-            elif in_getter != "" and s.startswith("get"):
-                t = ""
-                for i in range(0, lastindent):
-                    t += " "                
-                if len(s) > 3: rest = s[3:]
-                else: rest = ""
-                subst_getters(rest, getters)
-                rest = type_replace(rest)
-                rest = rename_native(rest)
-                rest = replace_generals(rest)
-                rest = enum_replace(rest)
-                if  in_bracket_op:
-                    tgt.write(t + in_getter_type + " " + in_getter + " " + rest + "\n")
-                else:
-                    tgt.write(t + in_getter_type + " " + in_getter + "() " + rest + "\n")
-                if rest.find("}") == -1:
-                    in_getter_get = 1
-            elif in_getter != "" and s.startswith("set"):
-                t = ""
-                for i in range(0, lastindent):
-                    t += " "
-                if len(s) > 3: rest = type_replace(s[3:])
-                else: rest = ""
-                subst_getters(rest, getters)
-                rest = rest.replace("(Integer)value", "Integer(value)")
-                rest = type_replace(rest)
-                rest = rename_native(rest)
-                rest = replace_generals(rest)
-                rest = enum_replace(rest)
-                ac_acc = in_getter_type[:in_getter_type.find(' ')]
-                ac_type = in_getter_type[in_getter_type.find(' ')+1:]
-                if  in_bracket_op:
-                    in_getter = in_getter.replace("get", "set").replace(")", "")
-                    tgt.write(t + ac_acc + " void " + in_getter + ", " + ac_type + " value) " + rest + "\n")
-                else:
-                    tgt.write(t + ac_acc + " void set" + in_getter + "(" + ac_type + " value) " + rest + "\n")
-                if rest.find("}") == -1:
-                    in_getter_set = 1
-            elif in_getter != "" and in_getter_get == 1 and s == "}":
-                tgt.write(line)
-                in_getter_get = 0
-            elif in_getter != "" and in_getter_set == 1 and s == "}":
-                tgt.write(line)
-                in_getter_set = 0
-            elif in_getter != "" and in_getter_get == 0 and in_getter_set == 0 and s == "}":
-                in_getter = ""
-                in_getter_type == ""
-                in_bracket_op = 0
-                skip_brace = 0
-            elif s.startswith("uint ") and s.find("=") == -1:
-                line = line.replace("uint", "Integer", line)
-                line = re.sub("(?P<n>\w+)(?P<c>[,;])", "\g<n>\g<c>", line)
-                tgt.write(line);
-            elif (not in_class and (s.startswith("{") or s.startswith("}"))) or s.startswith("[") or s.startswith("#"):
-                # tgt.write("// Skipping: " + s)
-                pass
-            elif line == "}\n":
-                pass
-            else:
-                # indent = line.find(s)
-                # tgt.write("// LINE: " + line)
-                if line.find(": base") != -1:
-                    line = re.sub(": base\((?P<p>[^\{]*)\)", "{ super(\g<p>);", line)
-                    line = line[4:]
-                    obraces = line.count("{")
-                    cbraces = line.count("}")
-                    mbraces = obraces - cbraces
-                    # tgt.write("// obraces = " + str(obraces) + "\n")
-                    if obraces == 1:
-                        skip_brace = 1
-                    else:
-                        for i in range(0, mbraces):
-                            line = line.replace("\n", "}\n")
-                if (s.find("public") != -1 or s.find("protected") != -1 or s.find("internal") != -1) and s.find("(") != -1:
-                    line = re.sub(" = [\w.]+(?P<d>[,;\)])", "\g<d>", line)
-                a = type_replace(line)
-                a = enum_replace(a)
-                a = re.sub("(?P<d>[\(, ])params ", "\g<d>", a)
-                a = a.replace("base.", "super.")
-                a = re.sub("Contract.\w+\([\s\S]*\);", "", a)
-                a = rename_native(a)
-                a = re.sub("~\w+\(\)", "protected void finalize()", a)
-
-                if missing_foreach_brace == 1:
-                    # a = a.replace("\n", " // checked " + str(foreach_opened_brace) + "\n")
-                    if foreach_opened_brace == 0 and a.find("{") != -1:
-                        foreach_opened_brace = 1
-                    elif foreach_opened_brace == 0 and a.find("}") == -1:
-                        a = a.replace("\n", "}}\n")
-                        foreach_opened_brace = 0
-                        missing_foreach_brace = 0
-                    elif foreach_opened_brace == 1 and a.find("}") != -1:
-                        a = a.replace("\n", "}}\n")
-                        foreach_opened_brace = 0
-                        missing_foreach_brace = 0
-
-#                if a.find("foreach") != -1:
-#                   missing_foreach_brace = 1
-#                a = re.sub("foreach\s*\((?P<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
- #                          "{ Iterator fe_i = \g<w>.iterator(); while (fe_i.hasNext()) { \g<t> \g<i> = (long)fe_i.next(); ",
-#                           a)
-                a = re.sub("foreach\s*\((?P<t>[\w <>,]+)\s+(?P<i>\w+)\s+in\s+(?P<w>\w+)\)",
-                           "for (\g<t> \g<i>: \g<w>)",
-                           a)
-                if a.find("long o: m_queue") != -1:
-                    a = a.replace("long", "Long")
-                a = a.replace("readonly ", "")
-                a = a.replace("const ", "final ")
-                a = a.replace("String ToString", "String toString")
-                a = a.replace(".ToString", ".toString")
-                a = a.replace("internal ", "")
-                a = a.replace("new static", "static")
-                a = a.replace("new public", "public")
-                a = a.replace("override ", "")
-                a = a.replace("virtual ", "")
-                a = a.replace("o as AST", "(AST) o")
-                a = a.replace("o as Sort", "(Sort) o")
-                a = a.replace("other as AST", "(AST) other")
-                a = a.replace("o as FuncDecl", "(FuncDecl) o")
-                a = a.replace("IntPtr obj", "long obj")
-                a = a.replace("IntPtr o", "long o")
-                a = a.replace("new long()", "0")
-                a = a.replace("long.Zero", "0")
-                a = a.replace("object o", "Object o")
-                a = a.replace("object other", "Object other")
-                a = a.replace("IntPtr res = IntPtr.Zero;", "Native.IntPtr res = new Native.IntPtr();")
-                a = a.replace("out res", "res")
-                a = a.replace("GC.ReRegisterForFinalize(m_ctx);", "")
-                a = a.replace("GC.SuppressFinalize(this);", "")
-                a = a.replace(".Length", ".length")
-                a = a.replace("m_queue.Count", "m_queue.size()")
-                a = a.replace("m_queue.Add", "m_queue.add")
-                a = a.replace("m_queue.Clear", "m_queue.clear")
-                a = a.replace("for (long ", "for (int ")
-                a = a.replace("ReferenceEquals(Context, ctx)", "Context() == ctx")
-                a = a.replace("BigInteger.Parse", "new BigInteger")
-                if had_ulong_res == 0 and a.find("ulong res = 0") != -1:
-                    a = a.replace("ulong res = 0;", "LongPtr res = new LongPtr();")
-                elif had_ulong_res == 1:
-                    a = a.replace("ref res)", "res)")
-                    if a.find("return res;") != -1:
-                        a = a.replace("return res;", "return res.value;")
-                        had_ulong_res = 0
-                a = a.replace("lock (", "synchronized (")
-                if in_static_class:
-                    a = a.replace("static", "")
-                a = re.sub("ref (?P<id>\w+)", "\g<id>", a)
-                subst_getters(a, getters)
-                a = re.sub("NativeObject = (?P<rest>.*);", "setNativeObject(\g<rest>);", a)
-                a = replace_generals(a)
-                tgt.write(a)
-    tgt.close()
-
-mk_java_bindings()

src/api/ml/z3_theory_stubs.c

@@ -1,5 +1,5 @@
 /*++
-Copyright (c) 2010 Microsoft Corporation
+Copyright (c) Microsoft Corporation
 
 Module Name:
 

src/api/python/z3.py

@@ -38,7 +38,7 @@ Z3 exceptions:
 ...   n = x + y
 ... except Z3Exception as ex:
 ...   print("failed: %s" % ex)
-failed: 'sort mismatch'
+failed: sort mismatch
 """
 from z3core import *
 from z3types import *
@@ -1398,7 +1398,7 @@ def BoolVector(prefix, sz, ctx=None):
     return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
 
 def FreshBool(prefix='b', ctx=None):
-    """Return a fresh Bolean constant in the given context using the given prefix.
+    """Return a fresh Boolean constant in the given context using the given prefix.
     
     If `ctx=None`, then the global context is used.    
 

src/api/z3_algebraic.h

@@ -23,7 +23,19 @@ Notes:
 
 #ifdef __cplusplus
 extern "C" {
-#endif // __cplusplus
+#endif // __cplusplus    
+
+    /**
+    \defgroup capi C API
+
+    */
+
+    /*@{*/
+
+    /**
+    @name Algebraic Numbers API
+    */
+    /*@{*/
 
     /**
        \brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
@@ -218,6 +230,8 @@ extern "C" {
     */
     int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);    
 
+    /*@}*/
+    /*@}*/
 
 #ifdef __cplusplus
 };

src/api/z3_api.h

@@ -771,7 +771,6 @@ typedef enum
 
         The premises of the rules is a sequence of clauses.
         The first clause argument is the main clause of the rule.
-        One literal from the second, third, .. clause is resolved
         with a literal from the first (main) clause.
 
         Premises of the rules are of the form
@@ -1143,8 +1142,8 @@ typedef enum {
    - Z3_FILE_ACCESS_ERRROR: A file could not be accessed.
    - Z3_INVALID_USAGE:   API call is invalid in the current state.
    - Z3_INTERNAL_FATAL: An error internal to Z3 occurred.
-   - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized\mlonly.\endmlonly\conly with #Z3_inc_ref.
+   - Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized \mlonly.\endmlonly \conly with #Z3_inc_ref.
-   - Z3_EXCEPTION:     Internal Z3 exception. Additional details can be retrieved using \mlonly #Z3_get_error_msg. \endmlonly \conly #Z3_get_error_msg_ex.
+   - Z3_EXCEPTION:     Internal Z3 exception. Additional details can be retrieved using #Z3_get_error_msg.
 */
 typedef enum
 {
@@ -1287,8 +1286,6 @@ extern "C" {
 
        \sa Z3_global_param_set
 
-       The caller must invoke #Z3_global_param_del_value to delete the value returned at \c param_value.
-
        \remark This function cannot be invoked simultaneously from different threads without synchronization.
        The result string stored in param_value is stored in shared location.
 

src/api/z3_interp.h

@@ -24,7 +24,14 @@ extern "C" {
 #endif // __cplusplus
 
     /**
-        @name Interpolation
+    \defgroup capi C API
+
+    */
+
+    /*@{*/
+
+    /**
+        @name Interpolation API
         */
     /*@{*/
 
@@ -184,6 +191,8 @@ extern "C" {
        \param cnsts Returns sequence of formulas (do not free)
        \param parents Returns the parents vector (or NULL for sequence)
        \param error Returns an error message in case of failure (do not free the string)
+       \param num_theory Number of theory terms
+       \param theory Theory terms
 
        Returns true on success.
 
@@ -232,6 +241,8 @@ extern "C" {
         \param parents The parents vector (or NULL for sequence)
         \param interps The interpolant to check
         \param error Returns an error message if interpolant incorrect (do not free the string)
+        \param num_theory Number of theory terms
+        \param theory Theory terms
 
         Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if
         incorrect, and Z3_L_UNDEF if unknown.
@@ -258,6 +269,8 @@ extern "C" {
         \param cnsts Array of constraints
         \param parents The parents vector (or NULL for sequence)
         \param filename The file name to write
+        \param num_theory Number of theory terms
+        \param theory Theory terms
 
         def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST)))
         */
@@ -270,6 +283,9 @@ extern "C" {
                                                 __in unsigned num_theory,
                                                 __in_ecount(num_theory) Z3_ast theory[]);
 
+    /*@}*/
+    /*@}*/
+
 #ifdef __cplusplus
 };
 #endif // __cplusplus

src/api/z3_polynomial.h

@@ -24,6 +24,19 @@ Notes:
 extern "C" {
 #endif // __cplusplus
 
+    /**
+    \defgroup capi C API
+
+    */
+
+    /*@{*/
+
+
+    /**
+    @name Polynomials API
+    */
+    /*@{*/
+
     /**
        \brief Return the nonzero subresultants of \c p and \c q with respect to the "variable" \c x.
        
@@ -38,6 +51,9 @@ extern "C" {
     Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x);
 
 
+    /*@}*/
+    /*@}*/
+
 #ifdef __cplusplus
 };
 #endif // __cplusplus

src/api/z3_rcf.h

@@ -25,6 +25,18 @@ Notes:
 #ifdef __cplusplus
 extern "C" {
 #endif // __cplusplus
+    
+    /**
+    \defgroup capi C API
+
+    */
+
+    /*@{*/
+
+    /**
+    @name Real Closed Fields API
+    */
+    /*@{*/
 
     /**
        \brief Delete a RCF numeral created using the RCF API.
@@ -192,6 +204,9 @@ extern "C" {
     */
     void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num * n, __out Z3_rcf_num * d);
 
+    /*@}*/
+    /*@}*/
+
 #ifdef __cplusplus
 };
 #endif // __cplusplus

src/ast/float_decl_plugin.cpp

@@ -40,11 +40,10 @@ void float_decl_plugin::set_manager(ast_manager * m, family_id id) {
     SASSERT(m_int_sort != 0); // arith_decl_plugin must be installed before float_decl_plugin.
     m_manager->inc_ref(m_int_sort);
     
-    if (m_manager->has_plugin(symbol("bv"))) {
+    // BV is not optional anymore.
-        // bv plugin is optional, so m_bv_plugin may be 0
+    SASSERT(m_manager->has_plugin(symbol("bv")));        
         m_bv_fid = m_manager->mk_family_id("bv");
         m_bv_plugin = static_cast<bv_decl_plugin*>(m_manager->get_plugin(m_bv_fid));
-    }
 }
 
 float_decl_plugin::~float_decl_plugin() {
@@ -103,6 +102,18 @@ bool float_decl_plugin::is_value(expr * n, mpf & val) {
         m_fm.mk_nan(ebits, sbits, val);
         return true;
     }
+    else if (is_app_of(n, m_family_id, OP_FLOAT_PLUS_ZERO)) {
+        unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
+        unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
+        m_fm.mk_pzero(ebits, sbits, val);
+        return true;
+    }
+    else if (is_app_of(n, m_family_id, OP_FLOAT_MINUS_ZERO)) {
+        unsigned ebits = to_app(n)->get_decl()->get_range()->get_parameter(0).get_int();
+        unsigned sbits = to_app(n)->get_decl()->get_range()->get_parameter(1).get_int();
+        m_fm.mk_nzero(ebits, sbits, val);
+        return true;
+    }
     return false;
 }
 
@@ -156,7 +167,7 @@ sort * float_decl_plugin::mk_float_sort(unsigned ebits, unsigned sbits) {
     parameter ps[2] = { p1, p2 };
     sort_size sz;
     sz = sort_size::mk_very_big(); // TODO: refine
-    return m_manager->mk_sort(symbol("FP"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps));
+    return m_manager->mk_sort(symbol("FloatingPoint"), sort_info(m_family_id, FLOAT_SORT, sz, 2, ps));
 }
 
 sort * float_decl_plugin::mk_rm_sort() {
@@ -176,6 +187,14 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
         return mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
     case ROUNDING_MODE_SORT:
         return mk_rm_sort();
+    case FLOAT16_SORT:
+        return mk_float_sort(5, 11);
+    case FLOAT32_SORT:
+        return mk_float_sort(8, 24);
+    case FLOAT64_SORT:
+        return mk_float_sort(11, 53);
+    case FLOAT128_SORT:
+        return mk_float_sort(15, 133);
     default:
         m_manager->raise_exception("unknown floating point theory sort");
         return 0;
@@ -229,17 +248,18 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par
     unsigned ebits = s->get_parameter(0).get_int();
     unsigned sbits = s->get_parameter(1).get_int();
     scoped_mpf val(m_fm);
-    if (k == OP_FLOAT_NAN) {
+
-        m_fm.mk_nan(ebits, sbits, val);
+    switch (k)
+    {
+    case OP_FLOAT_NAN: m_fm.mk_nan(ebits, sbits, val);
         SASSERT(m_fm.is_nan(val));
+        break;
+    case OP_FLOAT_MINUS_INF: m_fm.mk_ninf(ebits, sbits, val); break;
+    case OP_FLOAT_PLUS_INF: m_fm.mk_pinf(ebits, sbits, val); break;
+    case OP_FLOAT_MINUS_ZERO: m_fm.mk_nzero(ebits, sbits, val); break;
+    case OP_FLOAT_PLUS_ZERO: m_fm.mk_pzero(ebits, sbits, val); break;
     }
-    else if (k == OP_FLOAT_MINUS_INF) {
+
-        m_fm.mk_ninf(ebits, sbits, val);
-    }
-    else {
-        SASSERT(k == OP_FLOAT_PLUS_INF);
-        m_fm.mk_pinf(ebits, sbits, val);
-    }
     return mk_value_decl(val);
 }
 
@@ -248,14 +268,14 @@ func_decl * float_decl_plugin::mk_bin_rel_decl(decl_kind k, unsigned num_paramet
     if (arity != 2)
         m_manager->raise_exception("invalid number of arguments to floating point relation");
     if (domain[0] != domain[1] || !is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch");
+        m_manager->raise_exception("sort mismatch, expected equal FloatingPoint sorts as arguments");
     symbol name;
     switch (k) {
-    case OP_FLOAT_EQ: name = "==";  break;
+    case OP_FLOAT_EQ: name = "fp.eq";  break;
-    case OP_FLOAT_LT: name = "<";   break;
+    case OP_FLOAT_LT: name = "fp.lt";   break;
-    case OP_FLOAT_GT: name = ">";   break;        
+    case OP_FLOAT_GT: name = "fp.gt";   break;        
-    case OP_FLOAT_LE: name = "<=";  break;        
+    case OP_FLOAT_LE: name = "fp.lte";  break;        
-    case OP_FLOAT_GE: name = ">=";  break;        
+    case OP_FLOAT_GE: name = "fp.gte";  break;        
     default:
         UNREACHABLE();
         break;
@@ -270,17 +290,18 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
     if (arity != 1)
         m_manager->raise_exception("invalid number of arguments to floating point relation");
     if (!is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch");
+        m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
     symbol name;
     switch (k) {
-    case OP_FLOAT_IS_ZERO: name = "isZero";  break;
+    case OP_FLOAT_IS_ZERO: name = "fp.isZero";  break;
-    case OP_FLOAT_IS_NZERO: name = "isNZero";   break;
+    case OP_FLOAT_IS_NZERO: name = "fp.isNZero";   break;
-    case OP_FLOAT_IS_PZERO: name = "isPZero";   break;        
+    case OP_FLOAT_IS_PZERO: name = "fp.isPZero";   break;        
-    case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus";  break;
+    case OP_FLOAT_IS_NEGATIVE: name = "fp.isNegative";  break;
-    case OP_FLOAT_IS_NAN: name = "isNaN";  break;
+    case OP_FLOAT_IS_POSITIVE: name = "fp.isPositive";  break;
-    case OP_FLOAT_IS_INF: name = "isInfinite";  break;
+    case OP_FLOAT_IS_NAN: name = "fp.isNaN";  break;
-    case OP_FLOAT_IS_NORMAL: name = "isNormal";  break;
+    case OP_FLOAT_IS_INF: name = "fp.isInfinite";  break;
-    case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal";  break;
+    case OP_FLOAT_IS_NORMAL: name = "fp.isNormal";  break;
+    case OP_FLOAT_IS_SUBNORMAL: name = "fp.isSubnormal";  break;
     default:
         UNREACHABLE();
         break;
@@ -293,11 +314,11 @@ func_decl * float_decl_plugin::mk_unary_decl(decl_kind k, unsigned num_parameter
     if (arity != 1)
         m_manager->raise_exception("invalid number of arguments to floating point operator");
     if (!is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch"); 
+        m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); 
     symbol name;
     switch (k) {
-    case OP_FLOAT_ABS:    name = "abs";  break;
+    case OP_FLOAT_ABS: name = "fp.abs"; break;
-    case OP_FLOAT_UMINUS: name = "-";   break;
+    case OP_FLOAT_NEG: name = "fp.neg"; break;
     default:
         UNREACHABLE();
         break;
@@ -310,12 +331,12 @@ func_decl * float_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_paramete
     if (arity != 2)
         m_manager->raise_exception("invalid number of arguments to floating point operator");
     if (domain[0] != domain[1] || !is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch"); 
+        m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); 
     symbol name;
     switch (k) {
-    case OP_FLOAT_REM: name = "remainder";  break;
+    case OP_FLOAT_REM: name = "fp.rem"; break;
-    case OP_FLOAT_MIN: name = "fp.min";   break;
+    case OP_FLOAT_MIN: name = "fp.min"; break;
-    case OP_FLOAT_MAX: name = "fp.max";   break;
+    case OP_FLOAT_MAX: name = "fp.max"; break;
     default:
         UNREACHABLE();
         break;
@@ -327,14 +348,16 @@ func_decl * float_decl_plugin::mk_rm_binary_decl(decl_kind k, unsigned num_param
                                                  unsigned arity, sort * const * domain, sort * range) {
     if (arity != 3)
         m_manager->raise_exception("invalid number of arguments to floating point operator");
-    if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || !is_float_sort(domain[1]))
+    if (!is_rm_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch"); 
+        m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
+    if (domain[1] != domain[2] || !is_float_sort(domain[1]))
+        m_manager->raise_exception("sort mismatch, expected arguments 1 and 2 of equal FloatingPoint sorts"); 
     symbol name;
     switch (k) {
-    case OP_FLOAT_ADD: name = "+";   break;
+    case OP_FLOAT_ADD: name = "fp.add";   break;
-    case OP_FLOAT_SUB: name = "-";   break;
+    case OP_FLOAT_SUB: name = "fp.sub";   break;
-    case OP_FLOAT_MUL: name = "*";   break;
+    case OP_FLOAT_MUL: name = "fp.mul";   break;
-    case OP_FLOAT_DIV: name = "/";   break;
+    case OP_FLOAT_DIV: name = "fp.div";   break;
     default:
         UNREACHABLE();
         break;
@@ -346,12 +369,14 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame
                                                 unsigned arity, sort * const * domain, sort * range) {
     if (arity != 2)
         m_manager->raise_exception("invalid number of arguments to floating point operator");
-    if (!is_rm_sort(domain[0]) || !is_float_sort(domain[1]))
+    if (!is_rm_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch"); 
+        m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument");
+    if (!is_float_sort(domain[1]))
+        m_manager->raise_exception("sort mismatch, expected FloatingPoint as second argument"); 
     symbol name;
     switch (k) {
-    case OP_FLOAT_SQRT: name = "squareRoot";   break;
+    case OP_FLOAT_SQRT: name = "fp.sqrt";   break;
-    case OP_FLOAT_ROUND_TO_INTEGRAL: name = "roundToIntegral";   break;
+    case OP_FLOAT_ROUND_TO_INTEGRAL: name = "fp.roundToIntegral";   break;
     default:
         UNREACHABLE();
         break;
@@ -359,13 +384,15 @@ func_decl * float_decl_plugin::mk_rm_unary_decl(decl_kind k, unsigned num_parame
     return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k));
 }
 
-func_decl * float_decl_plugin::mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl * float_decl_plugin::mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                            unsigned arity, sort * const * domain, sort * range) {
     if (arity != 4)
         m_manager->raise_exception("invalid number of arguments to fused_ma operator");
-    if (!is_rm_sort(domain[0]) || domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1]))
+    if (!is_rm_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch"); 
+        m_manager->raise_exception("sort mismatch, expected RoundingMode as first argument");
-    symbol name("fusedMA");
+    if (domain[1] != domain[2] || domain[1] != domain[3] || !is_float_sort(domain[1]))
+        m_manager->raise_exception("sort mismatch, expected arguments 1,2,3 of equal FloatingPoint sort"); 
+    symbol name("fp.fma");
     return m_manager->mk_func_decl(name, arity, domain, domain[1], func_decl_info(m_family_id, k));
 }
 
@@ -375,12 +402,13 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
         is_sort_of(domain[0], m_bv_fid, BV_SORT) &&
         is_sort_of(domain[1], m_bv_fid, BV_SORT) &&
         is_sort_of(domain[2], m_bv_fid, BV_SORT)) {
-        // When the bv_decl_plugin is installed, then we know how to convert 3 bit-vectors into a float!        
+        // 3 BVs -> 1 FP
         sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1);
-        symbol name("asFloat");
+        symbol name("fp");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
     }
     else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) {
+        // 1 BV -> 1 FP
         if (num_parameters != 2)
             m_manager->raise_exception("invalid number of parameters to to_fp");
         if (!parameters[0].is_int() || !parameters[1].is_int())
@@ -389,37 +417,67 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters,
         int sbits = parameters[1].get_int();
         
         sort * fp = mk_float_sort(ebits, sbits);
-        symbol name("asFloat");
+        symbol name("to_fp");
+        return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
+    else if (m_bv_plugin && arity == 2 && 
+             is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+             is_sort_of(domain[1], m_bv_fid, BV_SORT)) {
+        // Rounding + 1 BV -> 1 FP
+        if (num_parameters != 2)
+            m_manager->raise_exception("invalid number of parameters to to_fp");
+        if (!parameters[0].is_int() || !parameters[1].is_int())
+            m_manager->raise_exception("invalid parameter type to to_fp");
+        int ebits = parameters[0].get_int();
+        int sbits = parameters[1].get_int();
+
+        sort * fp = mk_float_sort(ebits, sbits);
+        symbol name("to_fp");
+        return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
+    }
+    else if (arity == 2 &&
+             is_sort_of(domain[0], m_family_id, ROUNDING_MODE_SORT) &&
+             is_sort_of(domain[1], m_family_id, FLOAT_SORT)) {
+        // Rounding + 1 FP -> 1 FP
+        if (num_parameters != 2)
+            m_manager->raise_exception("invalid number of parameters to to_fp");
+        if (!parameters[0].is_int() || !parameters[1].is_int())
+            m_manager->raise_exception("invalid parameter type to to_fp");
+        int ebits = parameters[0].get_int();
+        int sbits = parameters[1].get_int();        
+        if (!is_rm_sort(domain[0]))
+            m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
+        if (!is_sort_of(domain[1], m_family_id, FLOAT_SORT))
+            m_manager->raise_exception("sort mismatch, expected second argument of FloatingPoint sort");
+        
+        sort * fp = mk_float_sort(ebits, sbits);
+        symbol name("to_fp");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));
     }
     else {
-        // .. Otherwise we only know how to convert rationals/reals. 
+        // 1 Real -> 1 FP
         if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) 
-            m_manager->raise_exception("expecting two integer parameters to asFloat");        
+            m_manager->raise_exception("expecting two integer parameters to to_fp");        
         if (arity != 2 && arity != 3)
-            m_manager->raise_exception("invalid number of arguments to asFloat operator");
+            m_manager->raise_exception("invalid number of arguments to to_fp operator");
         if (arity == 3 && domain[2] != m_int_sort)
-            m_manager->raise_exception("sort mismatch");     
+            m_manager->raise_exception("sort mismatch, expected second argument of Int sort");     
-        if (!is_rm_sort(domain[0]) ||
+        if (domain[1] != m_real_sort)
-            !(domain[1] == m_real_sort || is_sort_of(domain[1], m_family_id, FLOAT_SORT)))
+            m_manager->raise_exception("sort mismatch, expected second argument of Real sort");
-            m_manager->raise_exception("sort mismatch");
         
         sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
-        symbol name("asFloat");
+        symbol name("to_fp");
         return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters));            
     }
 }
 
-func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl * float_decl_plugin::mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                              unsigned arity, sort * const * domain, sort * range) {
-    if (!m_bv_plugin)
-        m_manager->raise_exception("asIEEEBV unsupported; use a logic with BV support");
     if (arity != 1)
         m_manager->raise_exception("invalid number of arguments to asIEEEBV");
     if (!is_float_sort(domain[0]))
-        m_manager->raise_exception("sort mismatch");
+        m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort");
-
+    
-    // When the bv_decl_plugin is installed, then we know how to convert a float to an IEEE bit-vector.
     unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int();
     parameter ps[] = { parameter(float_sz) };
     sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps);
@@ -429,41 +487,34 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter
 
 func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned arity, sort * const * domain, sort * range) {
-    if (!m_bv_plugin)
-        m_manager->raise_exception("fp unsupported; use a logic with BV support");
     if (arity != 3)
         m_manager->raise_exception("invalid number of arguments to fp");    
     if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) ||
         !is_sort_of(domain[1], m_bv_fid, BV_SORT) ||
         !is_sort_of(domain[2], m_bv_fid, BV_SORT))
-        m_manager->raise_exception("sort mismtach");
+        m_manager->raise_exception("sort mismatch");
         
     sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1);
     symbol name("fp");
     return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
 }
 
-func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                                  unsigned arity, sort * const * domain, sort * range) {
     if (!m_bv_plugin)
         m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support");
     if (arity != 2)
         m_manager->raise_exception("invalid number of arguments to to_fp_unsigned");
     if (is_rm_sort(domain[0]))
-        m_manager->raise_exception("sort mismtach");
+        m_manager->raise_exception("sort mismatch, expected first argument of RoundingMode sort");
     if (!is_sort_of(domain[1], m_bv_fid, BV_SORT))
-        m_manager->raise_exception("sort mismtach");
+        m_manager->raise_exception("sort mismatch, expected second argument of BV sort");
 
     sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
-    symbol name("to_fp_unsigned");
+    symbol name("fp.t_ubv");
     return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k));
 }
 
-func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
-    unsigned arity, sort * const * domain, sort * range) {
-    NOT_IMPLEMENTED_YET();
-}
-
 func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
     unsigned arity, sort * const * domain, sort * range) {
     NOT_IMPLEMENTED_YET();
@@ -498,14 +549,15 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
     case OP_FLOAT_IS_ZERO:
     case OP_FLOAT_IS_NZERO:
     case OP_FLOAT_IS_PZERO:
-    case OP_FLOAT_IS_SIGN_MINUS: 
+    case OP_FLOAT_IS_NEGATIVE: 
+    case OP_FLOAT_IS_POSITIVE:
     case OP_FLOAT_IS_NAN:
     case OP_FLOAT_IS_INF:
     case OP_FLOAT_IS_NORMAL:
     case OP_FLOAT_IS_SUBNORMAL:
         return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_ABS: 
-    case OP_FLOAT_UMINUS:
+    case OP_FLOAT_NEG:
         return mk_unary_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_REM:
     case OP_FLOAT_MIN:
@@ -517,20 +569,18 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
         return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_SUB:
         if (arity == 1) 
-            return mk_unary_decl(OP_FLOAT_UMINUS, num_parameters, parameters, arity, domain, range);
+            return mk_unary_decl(OP_FLOAT_NEG, num_parameters, parameters, arity, domain, range);
         else
             return mk_rm_binary_decl(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_SQRT:
     case OP_FLOAT_ROUND_TO_INTEGRAL:
         return mk_rm_unary_decl(k, num_parameters, parameters, arity, domain, range);
-    case OP_FLOAT_FUSED_MA:
+    case OP_FLOAT_FMA:
-        return mk_fused_ma(k, num_parameters, parameters, arity, domain, range);
+        return mk_fma(k, num_parameters, parameters, arity, domain, range);
-    case OP_TO_IEEE_BV:
+    case OP_FLOAT_TO_IEEE_BV:
-        return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
+        return mk_float_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_FP:
         return mk_from3bv(k, num_parameters, parameters, arity, domain, range);
-    case OP_FLOAT_TO_FP_UNSIGNED:
-        return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_TO_UBV:
         return mk_to_ubv(k, num_parameters, parameters, arity, domain, range);
     case OP_FLOAT_TO_SBV:
@@ -544,8 +594,11 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
 }
 
 void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
-    op_names.push_back(builtin_name("plusInfinity",  OP_FLOAT_PLUS_INF));
+    // These are the operators from the final draft of the SMT FloatingPoint standard
-    op_names.push_back(builtin_name("minusInfinity", OP_FLOAT_MINUS_INF));
+    op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
+    op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));
+    op_names.push_back(builtin_name("+zero", OP_FLOAT_PLUS_ZERO));
+    op_names.push_back(builtin_name("-zero", OP_FLOAT_MINUS_ZERO));
     op_names.push_back(builtin_name("NaN", OP_FLOAT_NAN));
 
     op_names.push_back(builtin_name("roundNearestTiesToEven", OP_RM_NEAREST_TIES_TO_EVEN));
@@ -554,46 +607,6 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("roundTowardNegative", OP_RM_TOWARD_NEGATIVE));
     op_names.push_back(builtin_name("roundTowardZero", OP_RM_TOWARD_ZERO));
     
-    op_names.push_back(builtin_name("+", OP_FLOAT_ADD)); 
-    op_names.push_back(builtin_name("-", OP_FLOAT_SUB)); 
-    op_names.push_back(builtin_name("/", OP_FLOAT_DIV)); 
-    op_names.push_back(builtin_name("*", OP_FLOAT_MUL)); 
-
-    op_names.push_back(builtin_name("abs", OP_FLOAT_ABS));     
-    op_names.push_back(builtin_name("remainder", OP_FLOAT_REM));  
-    op_names.push_back(builtin_name("fusedMA", OP_FLOAT_FUSED_MA));  
-    op_names.push_back(builtin_name("squareRoot", OP_FLOAT_SQRT));  
-    op_names.push_back(builtin_name("roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL));  
-    
-    op_names.push_back(builtin_name("==", OP_FLOAT_EQ));
-    
-    op_names.push_back(builtin_name("<",  OP_FLOAT_LT));
-    op_names.push_back(builtin_name(">",  OP_FLOAT_GT));
-    op_names.push_back(builtin_name("<=", OP_FLOAT_LE));
-    op_names.push_back(builtin_name(">=", OP_FLOAT_GE));
-
-    op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN));
-    op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF));
-    op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO));
-    op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO));
-    op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO));
-    op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL));
-    op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
-    op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
-
-    // Disabled min/max, clashes with user-defined min/max functions
-    // op_names.push_back(builtin_name("min", OP_FLOAT_MIN));
-    // op_names.push_back(builtin_name("max", OP_FLOAT_MAX));
-
-    op_names.push_back(builtin_name("asFloat", OP_TO_FLOAT));
-
-    if (m_bv_plugin)
-        op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV));
-
-    // These are the operators from the final draft of the SMT FloatingPoints standard
-    op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF));
-    op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF));
-
     op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN));
     op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY));
     op_names.push_back(builtin_name("RTP", OP_RM_TOWARD_POSITIVE));
@@ -601,44 +614,47 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
     op_names.push_back(builtin_name("RTZ", OP_RM_TOWARD_ZERO));
 
     op_names.push_back(builtin_name("fp.abs", OP_FLOAT_ABS));
-    op_names.push_back(builtin_name("fp.neg", OP_FLOAT_UMINUS)); 
+    op_names.push_back(builtin_name("fp.neg", OP_FLOAT_NEG)); 
     op_names.push_back(builtin_name("fp.add", OP_FLOAT_ADD)); 
     op_names.push_back(builtin_name("fp.sub", OP_FLOAT_SUB));     
     op_names.push_back(builtin_name("fp.mul", OP_FLOAT_MUL)); 
     op_names.push_back(builtin_name("fp.div", OP_FLOAT_DIV));
-    op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FUSED_MA)); 
+    op_names.push_back(builtin_name("fp.fma", OP_FLOAT_FMA)); 
     op_names.push_back(builtin_name("fp.sqrt", OP_FLOAT_SQRT)); 
     op_names.push_back(builtin_name("fp.rem", OP_FLOAT_REM));  
-    op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ));    
+    op_names.push_back(builtin_name("fp.roundToIntegral", OP_FLOAT_ROUND_TO_INTEGRAL));
+    op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
+    op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));      
     op_names.push_back(builtin_name("fp.leq", OP_FLOAT_LE));
     op_names.push_back(builtin_name("fp.lt",  OP_FLOAT_LT));    
     op_names.push_back(builtin_name("fp.geq", OP_FLOAT_GE));
     op_names.push_back(builtin_name("fp.gt",  OP_FLOAT_GT));
+    op_names.push_back(builtin_name("fp.eq", OP_FLOAT_EQ));
+
     op_names.push_back(builtin_name("fp.isNormal", OP_FLOAT_IS_NORMAL));
     op_names.push_back(builtin_name("fp.isSubnormal", OP_FLOAT_IS_SUBNORMAL));
     op_names.push_back(builtin_name("fp.isZero", OP_FLOAT_IS_ZERO));
     op_names.push_back(builtin_name("fp.isInfinite", OP_FLOAT_IS_INF));
     op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN));
-    op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN));
+    op_names.push_back(builtin_name("fp.isNegative", OP_FLOAT_IS_NEGATIVE));
-    op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX));
+    op_names.push_back(builtin_name("fp.isPositive", OP_FLOAT_IS_POSITIVE));    
-    op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT));
 
-    if (m_bv_plugin) {
+    op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
-        op_names.push_back(builtin_name("fp", OP_FLOAT_FP));
+    op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
-        op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED));
+    op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
-        op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV));
-        op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV));
-    }
         
-    // op_names.push_back(builtin_name("fp.toReal", ?));
+    op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT));    
 }
 
 void float_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
-    sort_names.push_back(builtin_name("FP", FLOAT_SORT));
+    sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT));
     sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT));
 
-    // In the SMT FPA final draft, FP is called FloatingPoint
+    // The final theory supports three common FloatingPoint sorts
-    sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT));
+    sort_names.push_back(builtin_name("Float16", FLOAT16_SORT));
+    sort_names.push_back(builtin_name("Float32", FLOAT32_SORT));
+    sort_names.push_back(builtin_name("Float64", FLOAT64_SORT));
+    sort_names.push_back(builtin_name("Float128", FLOAT128_SORT));
 }
 
 expr * float_decl_plugin::get_some_value(sort * s) {
@@ -662,6 +678,8 @@ bool float_decl_plugin::is_value(app * e) const {
     case OP_FLOAT_VALUE:
     case OP_FLOAT_PLUS_INF:
     case OP_FLOAT_MINUS_INF:
+    case OP_FLOAT_PLUS_ZERO:
+    case OP_FLOAT_MINUS_ZERO:
     case OP_FLOAT_NAN:
         return true;
     case OP_TO_FLOAT:

src/ast/float_decl_plugin.h

@@ -27,7 +27,11 @@ Revision History:
  
 enum float_sort_kind {
     FLOAT_SORT,
-    ROUNDING_MODE_SORT
+    ROUNDING_MODE_SORT,
+    FLOAT16_SORT,
+    FLOAT32_SORT,
+    FLOAT64_SORT,
+    FLOAT128_SORT
 };
 
 enum float_op_kind {
@@ -37,22 +41,23 @@ enum float_op_kind {
     OP_RM_TOWARD_NEGATIVE,
     OP_RM_TOWARD_ZERO,
 
-    
     OP_FLOAT_VALUE,
     OP_FLOAT_PLUS_INF,
     OP_FLOAT_MINUS_INF,
     OP_FLOAT_NAN,
+    OP_FLOAT_PLUS_ZERO,
+    OP_FLOAT_MINUS_ZERO,
     
     OP_FLOAT_ADD,
     OP_FLOAT_SUB,
-    OP_FLOAT_UMINUS,
+    OP_FLOAT_NEG,
     OP_FLOAT_MUL,
     OP_FLOAT_DIV,
     OP_FLOAT_REM,
     OP_FLOAT_ABS,
     OP_FLOAT_MIN,
     OP_FLOAT_MAX,
-    OP_FLOAT_FUSED_MA, // x*y + z
+    OP_FLOAT_FMA, // x*y + z
     OP_FLOAT_SQRT,
     OP_FLOAT_ROUND_TO_INTEGRAL,
 
@@ -68,13 +73,14 @@ enum float_op_kind {
     OP_FLOAT_IS_SUBNORMAL,    
     OP_FLOAT_IS_PZERO,
     OP_FLOAT_IS_NZERO,
-    OP_FLOAT_IS_SIGN_MINUS,
+    OP_FLOAT_IS_NEGATIVE,
+    OP_FLOAT_IS_POSITIVE,
 
     OP_TO_FLOAT,
-    OP_TO_IEEE_BV,
+    OP_FLOAT_TO_IEEE_BV,
 
     OP_FLOAT_FP,
-    OP_FLOAT_TO_FP_UNSIGNED,
+    OP_FLOAT_TO_FP,    
     OP_FLOAT_TO_UBV,
     OP_FLOAT_TO_SBV,
     OP_FLOAT_TO_REAL,
@@ -125,16 +131,14 @@ class float_decl_plugin : public decl_plugin {
                                   unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_rm_unary_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                  unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_fused_ma(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    func_decl * mk_fma(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                            unsigned arity, sort * const * domain, sort * range);
+                       unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_to_float(decl_kind k, unsigned num_parameters, parameter const * parameters,
                             unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
+    func_decl * mk_float_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                              unsigned arity, sort * const * domain, sort * range);
+                                    unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                            unsigned arity, sort * const * domain, sort * range);
-    func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
-                                  unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters,
                              unsigned arity, sort * const * domain, sort * range);
     func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters,
@@ -195,6 +199,7 @@ public:
     family_id get_fid() const { return m_fid; }
     family_id get_family_id() const { return m_fid; }
     arith_util & au() { return m_a_util; }
+    float_decl_plugin & plugin() { return *m_plugin; }
 
     sort * mk_float_sort(unsigned ebits, unsigned sbits);
     sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
@@ -242,16 +247,16 @@ public:
     app * mk_mul(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_MUL, arg1, arg2, arg3); }
     app * mk_sub(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_SUB, arg1, arg2, arg3); }
     app * mk_div(expr * arg1, expr * arg2, expr * arg3) { return m().mk_app(m_fid, OP_FLOAT_DIV, arg1, arg2, arg3); }
-    app * mk_uminus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_UMINUS, arg1); }
+    app * mk_neg(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_NEG, arg1); }
     app * mk_rem(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_REM, arg1, arg2); }
     app * mk_max(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MAX, arg1, arg2); }
     app * mk_min(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_MIN, arg1, arg2); }
     app * mk_abs(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_ABS, arg1); }
     app * mk_sqrt(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_SQRT, arg1, arg2); }
     app * mk_round(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_ROUND_TO_INTEGRAL, arg1, arg2); }
-    app * mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) {
+    app * mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4) {
         expr * args[4] = { arg1, arg2, arg3, arg4 };
-        return m().mk_app(m_fid, OP_FLOAT_FUSED_MA, 4, args);
+        return m().mk_app(m_fid, OP_FLOAT_FMA, 4, args);
     }
 
     app * mk_float_eq(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_EQ, arg1, arg2); }
@@ -267,11 +272,13 @@ public:
     app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); }
     app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); }
     app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); }
-    app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }
+    app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); }
+    app * mk_is_positive(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_POSITIVE, arg1); }
+    app * mk_is_negative(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NEGATIVE, arg1); }
 
-    bool is_uminus(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_UMINUS); }
+    bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); }
     
-    app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_TO_IEEE_BV, arg1); }
+    app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); }
 };
 
 #endif

src/ast/fpa/fpa2bv_converter.cpp

@@ -136,12 +136,13 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
         unsigned sbits = m_util.get_sbits(srt);
         
         expr_ref sgn(m), s(m), e(m);
-        sort_ref s_sgn(m), s_sig(m), s_exp(m);
-        s_sgn =  m_bv_util.mk_sort(1);
-        s_sig = m_bv_util.mk_sort(sbits-1);
-        s_exp = m_bv_util.mk_sort(ebits);
 
 #ifdef Z3DEBUG
+        sort_ref s_sgn(m), s_sig(m), s_exp(m);
+        s_sgn =  m_bv_util.mk_sort(1);
+        s_sig = m_bv_util.mk_sort(sbits - 1);
+        s_exp = m_bv_util.mk_sort(ebits);
+
         std::string p("fpa2bv");
         std::string name = f->get_name().str();
         
@@ -149,9 +150,17 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
         s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig);
         e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp);
 #else
-        sgn = m.mk_fresh_const(0, s_sgn);
+        expr_ref bv(m);
-        s = m.mk_fresh_const(0, s_sig);
+        unsigned bv_sz = 1 + ebits + (sbits - 1);
-        e = m.mk_fresh_const(0, s_exp);
+        bv = m.mk_fresh_const(0, m_bv_util.mk_sort(bv_sz));
+
+        sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
+        e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
+        s = m_bv_util.mk_extract(sbits - 2, 0, bv);
+
+        SASSERT(m_bv_util.get_bv_size(sgn) == 1);
+        SASSERT(m_bv_util.get_bv_size(s) == sbits-1);
+        SASSERT(m_bv_util.get_bv_size(e) == ebits);
 #endif
         
         mk_triple(sgn, s, e, result);
@@ -595,12 +604,12 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
 void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 3);
     expr_ref t(m);
-    mk_uminus(f, 1, &args[2], t);
+    mk_neg(f, 1, &args[2], t);
     expr * nargs[3] = { args[0], args[1], t };
     mk_add(f, 3, nargs, result);
 }
 
-void fpa2bv_converter::mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
     expr * sgn, * s, * e;
     split(args[0], sgn, s, e);
@@ -906,7 +915,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
     TRACE("fpa2bv_div", tout << "DIV = " << mk_ismt2_pp(result, m) << std::endl; );
 }
 
-void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 2);
     
     // Remainder is always exact, so there is no rounding mode.
@@ -1114,7 +1123,7 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
     mk_triple(r_sgn, r_sig, r_exp, result);
 }
 
-void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 4);
     
     // fusedma means (x * y) + z
@@ -1835,9 +1844,18 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const
     mk_is_denormal(args[0], result);
 }
 
-void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
     mk_is_neg(args[0], result);
+    TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;);
+}
+
+void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+    expr_ref t1(m), t2(m);
+    mk_is_nan(args[0], t1);
+    mk_is_pos(args[0], t2);
+    result = m.mk_and(m.mk_not(t1), t2);    
 }
 
 void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
@@ -2123,7 +2141,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
 void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
     SASSERT(num == 1);
     expr * sgn, * s, * e;
-    split(args[0], sgn, s, e);    
+    split(args[0], sgn, s, e);
     result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
 }
 
@@ -2132,19 +2150,55 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e
     mk_triple(args[0], args[2], args[1], result);
 }
 
-void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
-    NOT_IMPLEMENTED_YET();
-}
-
 void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 2);
+    SASSERT(f->get_num_parameters() == 1);
+    SASSERT(f->get_parameter(0).is_int());
+    
+    unsigned ebits = m_util.get_ebits(f->get_range());
+    unsigned sbits = m_util.get_sbits(f->get_range());
+    int width = f->get_parameter(0).get_int();
+
+    expr * rm = args[0];
+    expr * x = args[1];
+    
+    expr * sgn, *s, *e;
+    split(x, sgn, s, e);
+
     NOT_IMPLEMENTED_YET();
 }
 
 void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 2);
+    SASSERT(f->get_num_parameters() == 1);
+    SASSERT(f->get_parameter(0).is_int());
+
+    unsigned ebits = m_util.get_ebits(f->get_range());
+    unsigned sbits = m_util.get_sbits(f->get_range());
+    int width = f->get_parameter(0).get_int();
+
+    expr * rm = args[0];
+    expr * x = args[1];
+
+    expr * sgn, *s, *e;
+    split(x, sgn, s, e);
+
     NOT_IMPLEMENTED_YET();
 }
 
 void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+    SASSERT(num == 1);
+
+    unsigned ebits = m_util.get_ebits(f->get_range());
+    unsigned sbits = m_util.get_sbits(f->get_range());
+    int width = f->get_parameter(0).get_int();
+
+    expr * rm = args[0];
+    expr * x = args[1];
+
+    expr * sgn, *s, *e;
+    split(x, sgn, s, e);
+
     NOT_IMPLEMENTED_YET();
 }
 

src/ast/fpa/fpa2bv_converter.h

@@ -94,14 +94,14 @@ public:
 
     void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_uminus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_remainder(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_fusedma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
 
@@ -114,7 +114,8 @@ public:
     void mk_is_zero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
+    void mk_is_positive(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

src/ast/fpa/fpa2bv_rewriter.h

@@ -65,8 +65,6 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
 
     bool max_steps_exceeded(unsigned num_steps) const { 
         cooperate("fpa2bv");
-        if (memory::get_allocation_size() > m_max_memory)
-            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
         return num_steps > m_max_steps;
     }
 
@@ -117,17 +115,19 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FLOAT_VALUE: m_conv.mk_value(f, num, args, result); return BR_DONE;                             
             case OP_FLOAT_PLUS_INF: m_conv.mk_plus_inf(f, result); return BR_DONE;
             case OP_FLOAT_MINUS_INF: m_conv.mk_minus_inf(f, result); return BR_DONE;
+            case OP_FLOAT_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE;
+            case OP_FLOAT_MINUS_ZERO: m_conv.mk_nzero(f, result); return BR_DONE;
             case OP_FLOAT_NAN: m_conv.mk_nan(f, result); return BR_DONE;
             case OP_FLOAT_ADD: m_conv.mk_add(f, num, args, result); return BR_DONE;
             case OP_FLOAT_SUB: m_conv.mk_sub(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_UMINUS: m_conv.mk_uminus(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_NEG: m_conv.mk_neg(f, num, args, result); return BR_DONE;
             case OP_FLOAT_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE;
             case OP_FLOAT_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_REM: m_conv.mk_remainder(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE;
             case OP_FLOAT_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE;
             case OP_FLOAT_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE;
             case OP_FLOAT_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_FUSED_MA: m_conv.mk_fusedma(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE;
             case OP_FLOAT_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE;
             case OP_FLOAT_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE;
             case OP_FLOAT_EQ: m_conv.mk_float_eq(f, num, args, result); return BR_DONE;
@@ -142,18 +142,18 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
             case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
             case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE;
             case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE;
-            case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
+            case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
             case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
-            case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
             case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
             case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
             case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
             default:
                 TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n";
                       for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
-                throw tactic_exception("NYI");
+                NOT_IMPLEMENTED_YET();
             }
         }
 

src/ast/rewriter/float_rewriter.cpp

@@ -36,17 +36,17 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     br_status st = BR_FAILED;
     SASSERT(f->get_family_id() == get_fid());
     switch (f->get_decl_kind()) {
-    case OP_TO_FLOAT:        st = mk_to_float(f, num_args, args, result); break;
+    case OP_TO_FLOAT:        st = mk_to_fp(f, num_args, args, result); break;
     case OP_FLOAT_ADD:       SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
     case OP_FLOAT_SUB:       SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;
-    case OP_FLOAT_UMINUS:    SASSERT(num_args == 1); st = mk_uminus(args[0], result); break;
+    case OP_FLOAT_NEG:       SASSERT(num_args == 1); st = mk_neg(args[0], result); break;
     case OP_FLOAT_MUL:       SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break;
     case OP_FLOAT_DIV:       SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break;
     case OP_FLOAT_REM:       SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break;
     case OP_FLOAT_ABS:       SASSERT(num_args == 1); st = mk_abs(args[0], result); break;
     case OP_FLOAT_MIN:       SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break;
     case OP_FLOAT_MAX:       SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
-    case OP_FLOAT_FUSED_MA:  SASSERT(num_args == 4); st = mk_fused_ma(args[0], args[1], args[2], args[3], result); break;
+    case OP_FLOAT_FMA:       SASSERT(num_args == 4); st = mk_fma(args[0], args[1], args[2], args[3], result); break;
     case OP_FLOAT_SQRT:      SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
     case OP_FLOAT_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break;
 
@@ -62,10 +62,10 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     case OP_FLOAT_IS_INF:    SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
     case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
     case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
-    case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
+    case OP_FLOAT_IS_NEGATIVE: SASSERT(num_args == 1); st = mk_is_negative(args[0], result); break;
-    case OP_TO_IEEE_BV:      SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
+    case OP_FLOAT_IS_POSITIVE: SASSERT(num_args == 1); st = mk_is_positive(args[0], result); break;
+    case OP_FLOAT_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break;
     case OP_FLOAT_FP:        SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break;
-    case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break;
     case OP_FLOAT_TO_UBV:    SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break;
     case OP_FLOAT_TO_SBV:    SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break;
     case OP_FLOAT_TO_REAL:   SASSERT(num_args == 1); st = mk_to_real(args[0], result); break;
@@ -73,7 +73,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     return st;
 }
 
-br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+br_status float_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
     SASSERT(f->get_num_parameters() == 2);
     SASSERT(f->get_parameter(0).is_int());
     SASSERT(f->get_parameter(1).is_int());
@@ -154,7 +154,7 @@ br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref
 
 br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
     // a - b = a + (-b)
-    result = m_util.mk_add(arg1, arg2, m_util.mk_uminus(arg3));
+    result = m_util.mk_add(arg1, arg2, m_util.mk_neg(arg3));
     return BR_REWRITE2;
 }
 
@@ -188,7 +188,7 @@ br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref
     return BR_FAILED;
 }
 
-br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) {
+br_status float_rewriter::mk_neg(expr * arg1, expr_ref & result) {
     if (m_util.is_nan(arg1)) {
         // -nan --> nan
         result = arg1;
@@ -204,7 +204,7 @@ br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) {
         result = m_util.mk_plus_inf(m().get_sort(arg1));
         return BR_DONE;
     }
-    if (m_util.is_uminus(arg1)) {
+    if (m_util.is_neg(arg1)) {
         // - - a --> a
         result = to_app(arg1)->get_arg(0);
         return BR_DONE;
@@ -239,7 +239,7 @@ br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) {
         return BR_DONE;
     }
     result = m().mk_ite(m_util.mk_is_sign_minus(arg1),
-                        m_util.mk_uminus(arg1),
+                        m_util.mk_neg(arg1),
                         arg1);
     return BR_REWRITE2;
 }
@@ -284,7 +284,7 @@ br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
     return BR_REWRITE_FULL;
 }
 
-br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
+br_status float_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
     mpf_rounding_mode rm;
     if (m_util.is_rm_value(arg1, rm)) {
         scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
@@ -480,7 +480,7 @@ br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) {
     return BR_FAILED;
 }
 
-br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
+br_status float_rewriter::mk_is_negative(expr * arg1, expr_ref & result) {
     scoped_mpf v(m_util.fm());
     if (m_util.is_value(arg1, v)) {
         result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false();
@@ -490,6 +490,17 @@ br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
     return BR_FAILED;
 }
 
+br_status float_rewriter::mk_is_positive(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_neg(v) || m_util.fm().is_nan(v)) ? m().mk_false() : m().mk_true();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+
 // This the SMT =
 br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
     scoped_mpf v1(m_util.fm()), v2(m_util.fm());
@@ -532,10 +543,6 @@ br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref
     return BR_FAILED;
 }
 
-br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) {
-    return BR_FAILED;
-}
-
 br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) {
     return BR_FAILED;
 }

src/ast/rewriter/float_rewriter.h

@@ -45,17 +45,16 @@ public:
     br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
 
-    br_status mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
     br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
     br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
     br_status mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
-    br_status mk_uminus(expr * arg1, expr_ref & result);
+    br_status mk_neg(expr * arg1, expr_ref & result);
     br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_abs(expr * arg1, expr_ref & result);
     br_status mk_min(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_max(expr * arg1, expr * arg2, expr_ref & result);
-    br_status mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
+    br_status mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
     br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_round(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result);
@@ -70,10 +69,12 @@ public:
     br_status mk_is_inf(expr * arg1, expr_ref & result);
     br_status mk_is_normal(expr * arg1, expr_ref & result);
     br_status mk_is_subnormal(expr * arg1, expr_ref & result);
-    br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
+    br_status mk_is_negative(expr * arg1, expr_ref & result);
+    br_status mk_is_positive(expr * arg1, expr_ref & result);
 
     br_status mk_to_ieee_bv(expr * arg1, expr_ref & result);
 
+    br_status mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
     br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
     br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result);