mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 22:35:35 +00:00
Code Activity
4185 commits 23 branches 48 tags 157 MiB
Commit graph

4185 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 0a26bcf14c ensure unique symbols when MaxSAT problems are extracted from linear objectives such that multiple objectives can be supported. Fixes issue #308 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-13 15:12:08 -05:00
Nikolaj Bjorner 070d9183eb Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-11 11:39:49 -05:00
Nikolaj Bjorner 2865f60f8c deal with case of unsatisfiable context and bit-vector objectives that are not normalized to maxsmt. Issue #304 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-11 11:39:34 -05:00
Nikolaj Bjorner 1ad45783b1 Merge pull request #303 from NikolajBjorner/master 
toggle default for bv2int decision procedure support to avoid confusi…
 2015-11-10 15:10:43 -05:00
Nikolaj Bjorner 315dc80eb0 toggle default for bv2int decision procedure support to avoid confusing users. Issue #301 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-10 15:09:52 -05:00
Christoph M. Wintersteiger 746689904d Added elim_small_bv_tactic. 2015-11-10 16:23:05 +00:00
Christoph M. Wintersteiger faace0e6a3 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-09 19:44:40 +00:00
Christoph M. Wintersteiger 1807acdf26 tabs, whitespace 2015-11-09 17:50:50 +00:00
Nikolaj Bjorner 84f935ae85 initialize solver prior to translate. fixes build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-09 06:38:06 -08:00
Christoph M. Wintersteiger 5995c753d3 Bugfix for theory_fpa construction and destruction. 2015-11-09 13:54:28 +00:00
Christoph M. Wintersteiger 689ed9fa12 Added Z3_mk_array_ext to ML API. 
Relates to #292
 2015-11-09 13:49:37 +00:00
Christoph M. Wintersteiger cffff18373 -whitespace 2015-11-09 13:22:33 +00:00
Christoph M. Wintersteiger 6625f7a749 Added Z3_solver_translate to ML API. 2015-11-09 13:19:10 +00:00
Christoph M. Wintersteiger 4e05e93ecb Bugfix for FPA model generation/conversion. 
Addresses #300
 2015-11-09 11:52:44 +00:00
Nikolaj Bjorner e9315af0d9 remove tabs from z3.py to fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-08 04:22:44 -08:00
Nikolaj Bjorner 4685a5f8ba add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 16:42:13 -08:00
Nikolaj Bjorner 8d1fa3ae50 move mk_fresh to inside files that include smt_context.h directly to address build problem reported in #297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 11:50:06 -08:00
Nikolaj Bjorner 73c4e938ce Merge pull request #298 from NikolajBjorner/nsb/master 
Nsb/master
 2015-11-07 10:13:47 -08:00
Nikolaj Bjorner 13b19eb351 add translate facility to Java/C# APIs, request #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 10:10:21 -08:00
Nikolaj Bjorner c1adffb6ab Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-07 10:00:43 -08:00
Nikolaj Bjorner 1758799ef4 add translate facility to inc_sat_solver. Limit lemma copying to unit lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 10:00:14 -08:00
Nikolaj Bjorner 396875bedf fix compilation problem, issue #297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 22:56:53 -08:00
Nikolaj Bjorner 3d993a4ee1 Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-06 17:29:53 -08:00
Nikolaj Bjorner b4cb51cdb3 working on Forking/Serializing a z3 Solver #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 17:29:24 -08:00
Nikolaj Bjorner 5ea2c22153 fix build break - by renaming tout to out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 10:21:02 -08:00
Nikolaj Bjorner aeedb931f3 fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 10:20:21 -08:00
Christoph M. Wintersteiger a6b3fba038 Build fix, hide debug code in release mode. 2015-11-06 18:06:23 +00:00
Christoph M. Wintersteiger 05e7aca388 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-06 16:24:48 +00:00
Christoph M. Wintersteiger c2aee86e4e Added new SMT logic names 2015-11-06 16:24:44 +00:00
Nikolaj Bjorner deec11f24a Merge pull request #296 from NikolajBjorner/master 
fix for #291. The root issue is that the set of antecedents is recycl…
 2015-11-06 07:16:44 -08:00
Nikolaj Bjorner 7b72486644 Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-05 17:32:35 -08:00
Nikolaj Bjorner 63ea2c4d8f Merge pull request #295 from pazz/AstRef-hash 
add __hash__ to AstRef
 2015-11-05 16:20:10 -08:00
Nikolaj Bjorner fc592fc856 fix for #291. The root issue is that the set of antecedents is recycled as a fixed object between routines. Antecedents that were already allocated for a Gomory cut got reset by the internalizer. This causes unsound bounds axioms to be created 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-05 15:08:42 -08:00
Patrick Totzke d4242e16c5 add __hash__ to AstRef 
AstRef objects needs to be hashable in order
to be used as keys in python dictionaries
 2015-11-05 16:28:02 +00:00
Christoph M. Wintersteiger ebbed7a92e Added tactic comments for QF_AUFLIA, QF_AUFBV, QF_UF, and QF_UFBV default tactics. 2015-11-04 15:44:29 +00:00
Christoph M. Wintersteiger 7037739453 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-04 13:35:00 +00:00
Christoph M. Wintersteiger 715050da0b Java API comments fix. 2015-11-04 13:34:50 +00:00
Nikolaj Bjorner 9ca3596f18 Merge pull request #289 from NikolajBjorner/master 
fix rewriter for model validation
 2015-11-03 11:17:24 -08:00
Nikolaj Bjorner d6cb778365 fix rewriter for model validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-03 07:45:42 -08:00
Christoph M. Wintersteiger 2f216ee5c1 Fixed PREFIX for OSX installation. Fixes #124. 2015-11-03 15:35:43 +00:00
Christoph M. Wintersteiger bd94b59a92 Bugfix for arith rewriter to avoid rewriting loops. 2015-11-03 13:00:10 +00:00
Christoph M. Wintersteiger 27140c527c trailing whitespace 2015-11-03 12:56:29 +00:00
Christoph M. Wintersteiger 20715bbf3b Fixed initialization of interpolation context so it is properly disabled when solving SMT v1 benchmarks. 2015-11-03 12:29:02 +00:00
Christoph M. Wintersteiger 949ad4d2fc Trailing whitespace removed. 2015-11-03 12:28:10 +00:00
Nikolaj Bjorner 11b6676e8f Merge pull request #287 from NikolajBjorner/master 
Fix bug exposed by QF_NIA example
 2015-11-02 14:20:53 -08:00
Nikolaj Bjorner 2efd5bf9d1 Fix bug exposed in #281 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-02 14:18:49 -08:00
Nikolaj Bjorner f78c769b3b Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-02 13:49:48 -08:00
Christoph M. Wintersteiger 7ac64f1f96 Bugfix for FP model converter (fp.min/fp.max models) 2015-11-02 19:55:25 +00:00
Nikolaj Bjorner ec12368b54 Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-02 11:36:50 -08:00
Christoph M. Wintersteiger 92152b16ca Bugfixes for model verification of unspecified values of fp.min/fp.max 2015-11-02 19:25:44 +00:00