mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
4349 commits 49 branches 53 tags 182 MiB
Commit graph

4349 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
639dfc4b30 fix for string decoding in build scripts 2015-11-14 15:06:55 +00:00
Bernhard F. Brodowsky
f880433a69 Fixed typo in warning message. 2015-11-14 15:47:47 +01:00
Nikolaj Bjorner
2277a52d80 Merge pull request #309 from NikolajBjorner/master 
Fix for issue #308"
 2015-11-13 15:14:09 -05:00
Nikolaj Bjorner
54bb33615e Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-13 15:13:09 -05:00
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
Christoph M. Wintersteiger
27dcd8c5b6 Fix for python decoding of command line output strings 
Fixes #302
 2015-11-13 17:15:04 +00:00
Christoph M. Wintersteiger
15c48eeaf9 Fix for timeout/rlimit in deprecated solver API. 
Partially fixes #307.
 2015-11-13 16:42:46 +00:00
Christoph M. Wintersteiger
954400cfa2 whitespace 2015-11-13 16:35:08 +00:00
Christoph M. Wintersteiger
4cb96bfe76 Fixed assertion failure in fpa2bv_converter. 
Partially addresses #307
 2015-11-13 15:55:01 +00:00
Christoph M. Wintersteiger
806016c315 build fix 2015-11-13 14:11:39 +00:00
Christoph M. Wintersteiger
643dbb874b Added tactic that translates BV arrays into BV UFs. 2015-11-12 15:27:33 +00:00
Christoph M. Wintersteiger
5f8f0b1280 Added bool rewriter case. 2015-11-12 14:49:21 +00:00
Christoph M. Wintersteiger
5cf2caa7e9 Added check for QF_BV in QF_UFBV tactic. 2015-11-12 14:48:55 +00:00
Christoph M. Wintersteiger
87ae5888ee whitespace 2015-11-12 14:48:29 +00:00
Nikolaj Bjorner
be2d215fac Merge pull request #305 from NikolajBjorner/master 
deal with case of unsatisfiable context and bit-vector objectives tha…
 2015-11-11 11:41:26 -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