From 2cb84280d811229ec60418eed5de0b08c903d09a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 21 Jan 2015 17:58:31 +0000 Subject: [PATCH] Final adjustments for the FP integration Signed-off-by: Christoph M. Wintersteiger --- RELEASE_NOTES | 4 +- doc/mk_api_doc.py | 2 + doc/z3api.dox | 33 +--- src/api/java/Context.java | 23 +-- src/api/java/Fixedpoint.java | 2 +- src/api/z3_api.h | 2 +- src/api/z3_fpa.h | 342 ++++++++++++++++++----------------- 7 files changed, 192 insertions(+), 216 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index f185983a3..f8cac4c8b 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -3,11 +3,13 @@ RELEASE NOTES Version 4.4 ============= +- 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. -- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, and Codeplex users rsas, clockish, Heizmann. +- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, and Codeplex users rsas, clockish, Heizmann. Version 4.3.2 ============= diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 633f96c6b..476f2c8c7 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -31,6 +31,7 @@ try: 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 @@ try: 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 index dbaa3c8b8..cb4569dc4 100644 --- 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/src/api/java/Context.java b/src/api/java/Context.java index f7fa471fb..26a54b9c6 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -2000,25 +2000,22 @@ public class Context extends IDisposable /** * Create a universal Quantifier. + * @param sorts the sorts of the bound variables. + * @param names names of the bound variables + * @param body the body of the quantifier. + * @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. + * @param patterns array containing the patterns created using {@code MkPattern}. + * @param noPatterns array containing the anti-patterns created using {@code MkPattern}. + * @param quantifierID optional symbol to track quantifier. + * @param skolemID optional symbol to track skolem constants. + * * Remarks: Creates a forall formula, where * {@code weight"/> is the weight,