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

4610 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner e786d11183 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-10 21:07:14 -08:00
Nikolaj Bjorner 131f9e2247 change queries to take function names instead of arbitrary predicates. This allows to bypass issues with having arbitrary query expressions compiled in arbitrary ways to auxiliary predicates where names of bound variables are reshuffled. See also Stackoverflow http://stackoverflow.com/questions/34693719/bug-in-z3-datalog 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-10 20:43:41 -08:00
Nikolaj Bjorner e88ac377c5 Merge pull request #375 from delcypher/tidy_up_readme 
Tidy up readme
 2016-01-10 19:56:03 -08:00
Nikolaj Bjorner 082dcda7f7 Fix Issue #405: Horn normal form ignores implication 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-10 19:16:59 -08:00
Nikolaj Bjorner fce286db91 Issue #354. Fix unsoundness in Array theory based on missing propagation of selects over ite expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-10 17:11:12 -08:00
Nikolaj Bjorner 0df4931c4b dealing with issue #402 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-09 15:43:47 -08:00
Nikolaj Bjorner 20cfbcd66b dealing with issues #402 #399 #258 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-09 13:29:44 -08:00
Nikolaj Bjorner fc4260e018 enable Horner evaluation also for mixed-integer constraints now that ast-manger inserts coercions on the fly. Avoids loop for issue #399, but with this alone results in unknown status 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-09 10:01:44 -08:00
Nikolaj Bjorner aecab2b35b Merge pull request #408 from delcypher/optional_python_bindings 
Optional python bindings
 2016-01-08 20:40:41 -08:00
Nikolaj Bjorner 03cef7b03c add some conveniences for expressing string constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-08 16:19:32 -08:00
Nikolaj Bjorner e1ade258a0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-08 16:07:58 -08:00
Nikolaj Bjorner 4939957f6a check that disequations are solved 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-08 16:07:42 -08:00
Nikolaj Bjorner 52284922a0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-08 13:39:34 -08:00
Nikolaj Bjorner 9fb3d36961 pin expressions during substitution. Issue #367 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-08 13:39:23 -08:00
Dan Liew 49a2ed01c8 Improve error message emitting during configure when the Python 
bindings are enabled and the set python package directory does
not live under the install prefix. This is the other part required
to fix issue #404.
 2016-01-08 21:21:54 +00:00
Dan Liew e9ea687bb9 Disable the Python bindings by default which partially fixes issue #404. 
To enable the Python bindings use the newly added ``--python`` option.
 2016-01-08 21:21:54 +00:00
Nikolaj Bjorner 3d01246f71 Skip propagation on bits that have not (yet) been fixed by the SAT core: congruence closure for bits has not necessarily propagated to all bit positions when a bit in a congruence class gets fixed. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-08 08:17:18 -08:00
Christoph M. Wintersteiger 7e3676e24a bugfix for ML example 2016-01-08 13:25:14 +00:00
Nikolaj Bjorner 98f750f90d ml build failure, issue #403 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-07 20:37:47 -08:00
Nikolaj Bjorner 183d3821ce ml build failure, issue #403 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-07 20:14:43 -08:00
Nikolaj Bjorner 17a32a4e5f ml build failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-07 20:14:16 -08:00
Nikolaj Bjorner 023c564839 Issue #406 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-07 20:10:54 -08:00
Nikolaj Bjorner 0e6aaf0211 Issue #407 build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-07 20:05:49 -08:00
Nikolaj Bjorner 8b66411c05 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-07 16:04:35 -08:00
Nikolaj Bjorner ad778f87c7 change data-structures to concanetation decomposition normal form 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-07 16:03:37 -08:00
Christoph M. Wintersteiger 66604fa621 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-07 15:58:34 +00:00
Christoph M. Wintersteiger e53b580cb4 added compiler macro to disable invocation of the debugger upon failure. 2016-01-07 15:58:10 +00:00
Nikolaj Bjorner 0c2334417c fix build warnigs with && vs ||, tuning seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-07 06:53:00 -08:00
Nikolaj Bjorner 643999860d fix memory leak in SAT solver exposed by regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-06 17:32:54 -08:00
Nikolaj Bjorner 00f3a1fe81 fix memory leak in SAT solver exposed by regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-06 11:47:45 -08:00
Nikolaj Bjorner aec5a38b14 fix memory leak in SAT solver exposed by regression tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-06 11:44:55 -08:00
Nikolaj Bjorner da63ac809e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-05 10:16:12 -08:00
Nikolaj Bjorner fafdbfaf0e reset out_bits when blasting multiplication of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 10:16:02 -08:00
Christoph M. Wintersteiger 8b8dc95986 Merge pull request #398 from wintersteiger/jan4 
Improvements for the FPA API.
 2016-01-05 18:08:05 +00:00
Nikolaj Bjorner 9dfcaaa01d reset out_bits when blasting multiplication of bit-vectors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 10:07:44 -08:00
Christoph M. Wintersteiger de3cb7e5dc More FPA exponent/siginficand order consistency 2016-01-05 18:05:21 +00:00
Christoph M. Wintersteiger 1610e4fbd0 Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 17:45:35 +00:00
Nikolaj Bjorner ee157e47e4 fix crash caused by recycling variable names. Stackoverflow segfault-in-bv-rewritermk-mul-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 09:19:21 -08:00
Nikolaj Bjorner 65de39f403 disabling mk_const_case_multiplier until debugged 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 08:45:10 -08:00
Christoph M. Wintersteiger d176c8714a Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 16:38:12 +00:00
Nikolaj Bjorner 752a973e53 missing files? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 08:32:48 -08:00
Nikolaj Bjorner b0d244c1e0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-05 08:23:50 -08:00
Nikolaj Bjorner af758dea4a tuning for seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-05 08:23:44 -08:00
Nuno Lopes 465d28e160 seq_decl: fix build with stricter compilers 
get rid of 32 rellocations as a nice side-effect
 2016-01-05 14:57:41 +00:00
Christoph M. Wintersteiger b3a1aa27ee Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 14:48:52 +00:00
Christoph M. Wintersteiger 13cbd19411 FPA Python API cleanup. 2016-01-05 14:48:42 +00:00
Christoph M. Wintersteiger 3e000d7525 build fix for libz3.vcxproj 2016-01-05 14:40:31 +00:00
Nuno Lopes bc123dc79b fix build with c++98 compilers 2016-01-05 14:10:32 +00:00
Christoph M. Wintersteiger 097552768f Merged Python API changes. 2016-01-05 11:51:28 +00:00
Christoph M. Wintersteiger bd8a5982ad Added new items to .NET project file 2016-01-05 11:37:34 +00:00