mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity
4944 commits 23 branches 48 tags 157 MiB
Commit graph

4944 commits

This branch
This branch
All branches
Author SHA1 Message Date
Dan Liew
8ae60d300e Update information in `README.md` on ".NET" bindings. Since 
942b6ba5ec ``--dotnet`` needs to be
passed to enable the bindings.
 2016-01-11 23:50:37 +00:00
Dan Liew
cb106d71cf Teach the OCaml bindings install rule to respect the DESTDIR makefile 
variable. Previously it would try to install into the system (e.g.
``/usr/lib/ocaml``) regardless of the value of DESTDIR.

Unfortunately it looks like packagers who use DESTDIR to do staged
installs will need to have their packages patch their user's OCaml
``ld.conf`` file manually at package install time (not ``make install``
time) with the extra path to the Z3 Ocaml package directory. We could
use the ``touch`` command to create an empty ``ld.conf`` before running
``ocamlfind install`` but that adds the wrong path to ``ld.conf``
because it contains DESTDIR.
 2016-01-11 21:13:25 +00:00
Dan Liew
f038291293 Don't silently fail if ocamlfind cannot be found when building the Ocaml 
bindings is enabled. That is really unhelpful behaviour. Instead emit a
warning. I would prefer an error message but apparently being able to
build but not install the OCaml bindings is desirable.

Whilst I'm here also print information about ocamlfind where it should
have been mentioned.
 2016-01-11 19:36:02 +00:00
Nikolaj Bjorner
79a5b133d7 fix debugging code in ast.cpp to take into account that literals may be repeated 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-11 11:04:44 -08:00
Christoph M. Wintersteiger
d4efa3753c Optimization for real to float conversion. Relates to #383. 2016-01-11 18:54:07 +00:00
Mikolas Janota
b26e4b1516 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-11 18:27:47 +00:00
Nikolaj Bjorner
a156028d82 pin expressions per Sarah Winkler's memory leak report 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-11 09:46:10 -08:00
Nikolaj Bjorner
d4c98c1ab4 Corrected fix to #354: The parameters got shared between the MBQI checker and main context, overriding m_array_laziness to 0 which caused missing propagations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-11 09:38:05 -08:00
Mikolas Janota
edf6d63a0b Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-11 17:23:13 +00:00
mikolas
bbdd5ab96f Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-11 17:18:56 +00:00
mikolas
b46f312115 A proper model converter for the lazy mode. 2016-01-11 17:18:22 +00:00
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
Mikolas Janota
5706df30c6 Fixing soft timeout for check-sat-using. 2016-01-08 16:17:34 +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
Mikolas Janota
fbd02f6d5f Merge remote-tracking branch 'upstream/master' into lackr 2016-01-08 14:53:25 +00: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
Mikolas Janota
743a59254e Merge remote-tracking branch 'upstream/master' into lackr 2016-01-07 16:39:43 +00: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
George Karpenkov
f93c41b1be Since classes are non-final "instanceof" check is better in #equals 2016-01-06 11:27:58 +01:00
George Karpenkov
529b9d6833 The locking field should be final. 2016-01-06 11:19:38 +01:00
George Karpenkov
8bb0010dc3 Javadoc and indentation fixes 
- A proper way to refer to the function in the same class is "#funcName"

- There is no point in "@param p" declaration if no description follows
it.
 2016-01-06 11:19:26 +01:00
George Karpenkov
54e5bf2422 Remove redundant cast 2016-01-06 11:18:22 +01:00
George Karpenkov
93ad8d32b9 Remove redundant "throw" statement which has no effect. 2016-01-06 11:17:32 +01:00