pull unstable

Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
VeriFIT · Apr 1, 2015 · 52619b9 · 52619b9
2 parents 9c55be1 + 7fe337d
commit 52619b9
Show file tree

Hide file tree

Showing 337 changed files with 24,292 additions and 29,955 deletions.
diff --git a/.gitignore b/.gitignore
@@ -9,6 +9,7 @@ callgrind.out.*
 # OCaml generated files
 *.a
 *.cma
+*.cmo
 *.cmi
 *.cmxa
 ocamlz3
@@ -65,6 +66,12 @@ src/util/version.h
 src/api/java/Native.cpp
 src/api/java/Native.java
 src/api/java/enumerations/*.java
+src/api/ml/z3native_stubs.c
+src/api/ml/z3native.ml
+src/api/ml/z3enums.ml
+src/api/ml/z3native.mli
+src/api/ml/z3enums.mli
+src/api/ml/z3.mllib
 *.bak
 doc/api
 doc/code
diff --git a/README b/README
@@ -39,3 +39,6 @@ Remark: clang does not support OpenMP yet.
    CXX=clang++ CC=clang python scripts/mk_make.py
    cd build
    make
+
+
+To clean Z3 you can delete the build directory and run the mk_make.py script again.
diff --git a/RELEASE_NOTES b/RELEASE_NOTES
@@ -1,16 +1,25 @@
 RELEASE NOTES
 
-Version 4.3.3
+Version 4.4
 =============
 
-- Fixed bug in floating point models
+- New feature: Support for the theory of floating-point numbers. This comes in the form of logics (QF_FP and QF_FPBV), tactics (qffp and qffpbv), as well as a theory plugin that allows theory combinations. Z3 supports the official SMT theory definition of FP (see http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2) in SMT2 files, as well as all APIs.
+
+- New feature: Stochastic local search engine for bit-vector formulas (see the qfbv-sls tactic).
+  See also: Froehlich, Biere, Wintersteiger, Hamadi: Stochastic Local Search 
+  for Satisfiability Modulo Theories, AAAI 2015.
+
+- Upgrade: This release includes a brand new OCaml/ML API that is much better integrated with the build system, and hopefully also easier to use than the previous one.
+
+- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, Amir Ebrahimi, Codeplex users rsas, clockish, Heizmann, susmitj, steimann, and Stackoverflow users user297886.
+
 
 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. 
+- Added the interpolation features of iZ3, which are now integrated into 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

diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py
@@ -31,6 +31,7 @@ def cleanup_API(inf, outf):
     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')
+    cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h')
 
     print "Removed annotations from z3_api.h."
     try:
@@ -46,6 +47,7 @@ def cleanup_API(inf, outf):
     os.remove('tmp/z3_polynomial.h')
     os.remove('tmp/z3_rcf.h')
     os.remove('tmp/z3_interp.h')
+    os.remove('tmp/z3_fpa.h')
     print "Removed temporary file z3_api.h."
     os.remove('tmp/website.dox')	
     print "Removed temporary file website.dox"

diff --git a/doc/z3api.dox b/doc/z3api.dox
@@ -713,39 +713,10 @@ FILE_PATTERNS          = website.dox \
 			 z3_polynomial.h \
 			 z3_rcf.h \
 			 z3_interp.h \
+			 z3_fpa.h \
                          z3++.h \
                          z3py.py \
-                         ApplyResult.cs \
-                         AST.cs \
-                         ASTMap.cs \
-                         ASTVector.cs \
-                         Config.cs \
-                         Constructor.cs \
-                         Context.cs \
-                         DecRefQUeue.cs \
-                         Enumerations.cs \
-                         Expr.cs \
-                         FuncDecl.cs \
-                         FuncInterp.cs \
-                         Goal.cs \
-                         Log.cs \
-                         Model.cs \
-                         Native.cs \
-                         Numeral.cs \
-                         Params.cs \
-                         Pattern.cs \
-                         Probe.cs \
-                         Quantifier.cs \
-                         Solver.cs \
-                         Sort.cs \
-                         Statistics.cs \
-                         Status.cs \
-                         Symbol.cs \
-                         Tactic.cs \
-                         Util.cs \
-                         Version.cs \
-                         Z3Exception.cs \
-                         Z3Object.cs \
+						 *.cs \
                          *.java
 
 # The RECURSIVE tag can be used to turn specify whether or not subdirectories

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
@@ -1,9 +1,11 @@
 #include<vector>
 #include"z3++.h"
 
-
 using namespace z3;
 
+
+
+
 /**
    Demonstration of how Z3 can be used to prove validity of
    De Morgan's Duality Law: {e not(x and y) <-> (not x) or ( not y) }
@@ -999,7 +1001,17 @@ void opt_example() {
     }
 }
 
+void extract_example() {
+    std::cout << "extract example\n";
+    context c;
+    expr x(c);
+    x = c.constant("x", c.bv_sort(32));
+    expr y = x.extract(21, 10);
+    std::cout << y << " " << y.hi() << " " << y.lo() << "\n";
+}
+
 int main() {
+
     try {
         demorgan(); std::cout << "\n";
         find_model_example1(); std::cout << "\n";
@@ -1038,6 +1050,7 @@ int main() {
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";
         opt_example(); std::cout << "\n";
+        extract_example(); std::cout << "\n";
         std::cout << "done\n";
     }
     catch (exception & ex) {

diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c
@@ -2595,6 +2595,97 @@ void substitute_vars_example() {
     Z3_del_context(ctx);
 }
 
+/**
+   \brief Demonstrates some basic features of the FloatingPoint theory.
+*/
+
+void fpa_example() {
+    Z3_config cfg;
+    Z3_context ctx;
+    Z3_sort double_sort, rm_sort;
+    Z3_symbol s_rm, s_x, s_y, s_x_plus_y;
+    Z3_ast rm, x, y, n, x_plus_y, c1, c2, c3, c4, c5, c6;
+	Z3_ast args[2], args2[2], and_args[3], args3[3];
+
+    printf("\nFPA-example\n");
+    LOG_MSG("FPA-example");
+
+    cfg = Z3_mk_config();
+    ctx = Z3_mk_context(cfg);
+    Z3_del_config(cfg);
+
+    double_sort = Z3_mk_fpa_sort(ctx, 11, 53);
+    rm_sort = Z3_mk_fpa_rounding_mode_sort(ctx);
+
+	// Show that there are x, y s.t. (x + y) = 42.0 (with rounding mode).    
+	s_rm = Z3_mk_string_symbol(ctx, "rm");
+	rm = Z3_mk_const(ctx, s_rm, rm_sort);
+	s_x = Z3_mk_string_symbol(ctx, "x");
+	s_y = Z3_mk_string_symbol(ctx, "y");
+	x = Z3_mk_const(ctx, s_x, double_sort);
+	y = Z3_mk_const(ctx, s_y, double_sort);
+	n = Z3_mk_fpa_numeral_double(ctx, 42.0, double_sort);
+
+	s_x_plus_y = Z3_mk_string_symbol(ctx, "x_plus_y");
+	x_plus_y = Z3_mk_const(ctx, s_x_plus_y, double_sort);
+	c1 = Z3_mk_eq(ctx, x_plus_y, Z3_mk_fpa_add(ctx, rm, x, y));
+
+	args[0] = c1;
+	args[1] = Z3_mk_eq(ctx, x_plus_y, n);
+	c2 = Z3_mk_and(ctx, 2, (Z3_ast*)&args);
+
+	args2[0] = c2;
+	args2[1] = Z3_mk_not(ctx, Z3_mk_eq(ctx, rm, Z3_mk_fpa_rtz(ctx)));
+	c3 = Z3_mk_and(ctx, 2, (Z3_ast*)&args2);
+
+	and_args[0] = Z3_mk_not(ctx, Z3_mk_fpa_is_zero(ctx, y));
+	and_args[1] = Z3_mk_not(ctx, Z3_mk_fpa_is_nan(ctx, y));
+	and_args[2] = Z3_mk_not(ctx, Z3_mk_fpa_is_infinite(ctx, y));
+	args3[0] = c3;
+	args3[1] = Z3_mk_and(ctx, 3, and_args);
+	c4 = Z3_mk_and(ctx, 2, (Z3_ast*)&args3);
+
+	printf("c4: %s\n", Z3_ast_to_string(ctx, c4));
+	Z3_push(ctx);                  
+	Z3_assert_cnstr(ctx, c4);
+	check(ctx, Z3_L_TRUE);
+	Z3_pop(ctx, 1);
+
+	// Show that the following are equal:
+	//   (fp #b0 #b10000000001 #xc000000000000) 
+	//   ((_ to_fp 11 53) #x401c000000000000))
+	//   ((_ to_fp 11 53) RTZ 1.75 2)))
+	//   ((_ to_fp 11 53) RTZ 7.0)))
+
+	Z3_push(ctx);
+	c1 = Z3_mk_fpa_fp(ctx, 
+					  Z3_mk_numeral(ctx, "0", Z3_mk_bv_sort(ctx, 1)),
+					  Z3_mk_numeral(ctx, "3377699720527872", Z3_mk_bv_sort(ctx, 52)),
+					  Z3_mk_numeral(ctx, "1025", Z3_mk_bv_sort(ctx, 11)));
+	c2 = Z3_mk_fpa_to_fp_bv(ctx,
+							Z3_mk_numeral(ctx, "4619567317775286272", Z3_mk_bv_sort(ctx, 64)),
+							Z3_mk_fpa_sort(ctx, 11, 53));
+	c3 = Z3_mk_fpa_to_fp_int_real(ctx,
+                                  Z3_mk_fpa_rtz(ctx),
+								  Z3_mk_numeral(ctx, "2", Z3_mk_int_sort(ctx)),
+                                  Z3_mk_numeral(ctx, "1.75", Z3_mk_real_sort(ctx)),                                  
+                                  Z3_mk_fpa_sort(ctx, 11, 53));
+	c4 = Z3_mk_fpa_to_fp_real(ctx,
+							  Z3_mk_fpa_rtz(ctx),
+							  Z3_mk_numeral(ctx, "7.0", Z3_mk_real_sort(ctx)),
+							  Z3_mk_fpa_sort(ctx, 11, 53));
+	args3[0] = Z3_mk_eq(ctx, c1, c2);
+	args3[1] = Z3_mk_eq(ctx, c1, c3);
+	args3[2] = Z3_mk_eq(ctx, c1, c4);
+	c5 = Z3_mk_and(ctx, 3, args3);
+
+	printf("c5: %s\n", Z3_ast_to_string(ctx, c5));
+	Z3_assert_cnstr(ctx, c5);
+	check(ctx, Z3_L_TRUE);
+	Z3_pop(ctx, 1);
+
+    Z3_del_context(ctx);
+}
 
 /*@}*/
 /*@}*/
@@ -2640,5 +2731,6 @@ int main() {
     smt2parser_example();
     substitute_example();
     substitute_vars_example();
+    fpa_example();
     return 0;
 }