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

Conflicts: scripts/mk_project.py src/duality/duality.h src/duality/duality_solver.cpp src/duality/duality_wrapper.h src/interp/iz3hash.h Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
VeriFIT · Apr 25, 2014 · c3b7c73 · c3b7c73
2 parents 0915e6f + fceaf97
commit c3b7c73
Show file tree

Hide file tree

Showing 35 changed files with 11,884 additions and 11,582 deletions.
diff --git a/.gitattributes b/.gitattributes
@@ -1 +1,4 @@
+# Set default behaviour, in case users don't have core.autocrlf set.
+* text=auto
+
 src/api/dotnet/Properties/AssemblyInfo.cs text eol=crlf
diff --git a/.gitignore b/.gitignore
@@ -56,6 +56,8 @@ src/api/api_log_macros.cpp
 src/api/dll/api_dll.def
 src/api/dotnet/Enumerations.cs
 src/api/dotnet/Native.cs
+src/api/dotnet/Properties/AssemblyInfo.cs
+src/api/dotnet/Microsoft.Z3.xml
 src/api/python/z3consts.py
 src/api/python/z3core.py
 src/ast/pattern/database.h

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
@@ -43,17 +43,18 @@ def init_project_def():
     # Simplifier module will be deleted in the future.
     # It has been replaced with rewriter module.
     add_lib('simplifier', ['rewriter'], 'ast/simplifier')
+    add_lib('fpa', ['ast', 'util', 'simplifier'], 'ast/fpa')
     add_lib('macros', ['simplifier'], 'ast/macros')
     add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern')
     add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster')
     add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params')
     add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model')
     add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model',
-                    'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util'])
+                    'substitution', 'grobner', 'euclid', 'simplex', 'proof_checker', 'pattern', 'parser_util', 'fpa'])
     add_lib('user_plugin', ['smt'], 'smt/user_plugin')
     add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv')
     add_lib('fuzzing', ['ast'], 'test/fuzzing')
-    add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
+    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa')
     add_lib('smt_tactic', ['smt'], 'smt/tactic')
     add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
     add_lib('qe', ['smt','sat'], 'qe')
@@ -69,7 +70,7 @@ def init_project_def():
     add_lib('fp',  ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf'], 'muz/fp')
     add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
-    add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
+    add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
     add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic'], 'opt')
     API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
@@ -54,6 +54,7 @@ def getenv(name, default):
 IS_WINDOWS=False
 IS_LINUX=False
 IS_OSX=False
+IS_FREEBSD=False
 VERBOSE=True
 DEBUG_MODE=False
 SHOW_CPPS = True
@@ -98,6 +99,9 @@ def is_windows():
 def is_linux():
     return IS_LINUX
 
+def is_freebsd():
+    return IS_FREEBSD
+
 def is_osx():
     return IS_OSX
 
@@ -426,6 +430,8 @@ def check_eol():
         IS_OSX=True
     elif os.uname()[0] == 'Linux':
         IS_LINUX=True
+    elif os.uname()[0] == 'FreeBSD':
+        IS_FREEBSD=True
 
 def display_help(exit_code):
     print("mk_make.py: Z3 Makefile generator\n")
@@ -1181,6 +1187,8 @@ def mk_makefile(self, out):
                 t = t.replace('PLATFORM', 'darwin')
             elif IS_LINUX:
                 t = t.replace('PLATFORM', 'linux')
+            elif IS_FREEBSD:
+                t = t.replace('PLATFORM', 'freebsd')
             else:
                 t = t.replace('PLATFORM', 'win32')
             out.write(t)

diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py
@@ -144,7 +144,7 @@ def mk_z3_core(x64):
         cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64')
         cmds.append('cd %s' % BUILD_X64_DIR)    
     else:
-        cmds.append('"call %VCINSTALLDIR%vcvarsall.bat" x86')
+        cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" x86')
         cmds.append('cd %s' % BUILD_X86_DIR)
     cmds.append('nmake')
     if exec_cmds(cmds) != 0:

diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp
@@ -117,6 +117,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
         Z3_sort int_s = Z3_mk_int_sort(c);
         if (is_signed) {
             Z3_ast r = Z3_mk_bv2int(c, n, false);
+            Z3_inc_ref(c, r);
             Z3_sort s = Z3_get_sort(c, n);
             unsigned sz = Z3_get_bv_sort_size(c, s);
             rational max_bound = power(rational(2), sz);
@@ -135,6 +136,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) {                \
             Z3_dec_ref(c, pred);
             Z3_dec_ref(c, sub);
             Z3_dec_ref(c, zero);
+            Z3_dec_ref(c, r);
             RETURN_Z3(res);
         }
         else {

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
@@ -302,11 +302,11 @@ public ListSort MkListSort(string name, Sort elemSort)
         }
 
         /// <summary>
-        /// Create a new finite domain sort.
-	/// <param name="name">The name used to identify the sort</param>
-	/// <param size="size">The size of the sort</param>
-	/// <returns>The result is a sort</returns>
+        /// Create a new finite domain sort.	    
+	    /// <returns>The result is a sort</returns>
         /// </summary>
+        /// <param name="name">The name used to identify the sort</param>
+        /// <param name="size">The size of the sort</param>
         public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
         {
             Contract.Requires(name != null);
@@ -317,13 +317,13 @@ public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size)
         }
 
         /// <summary>
-        /// Create a new finite domain sort.
-	/// <param name="name">The name used to identify the sort</param>
-	/// <param size="size">The size of the sort</param>
-	/// <returns>The result is a sort</returns>
-	/// Elements of the sort are created using <seealso cref="MkNumeral"/>, 
-	/// and the elements range from 0 to <tt>size-1</tt>.
+        /// Create a new finite domain sort.	    
+	    /// <returns>The result is a sort</returns>
+	    /// Elements of the sort are created using <seealso cref="MkNumeral(ulong, Sort)"/>, 
+	    /// and the elements range from 0 to <tt>size-1</tt>.
         /// </summary>
+        /// <param name="name">The name used to identify the sort</param>
+        /// <param name="size">The size of the sort</param>
         public FiniteDomainSort MkFiniteDomainSort(string name, ulong size)
         {
             Contract.Ensures(Contract.Result<FiniteDomainSort>() != null);