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

4697 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
e2d54940b4 revert mixed integer/real handling pending fix to equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 12:11:27 -08:00
Dan Liew
250c8d028d Fix bug when configuring when building OCaml bindings is enabled 
when using Python2.

The output from ``check_output()`` has ``unicode`` type under
Python 2 but type ``str`` under Python 3. This type ended up being
used inside the ``MakeRuleCmd`` class which asserts that it receives
paths of type ``str``. To fix the problem under Python 2 the asserts
have been made weaker by also allowing the paths to be of type
``unicode``.
 2016-01-12 19:38:43 +00:00
Nikolaj Bjorner
f8971362c8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-12 11:19:04 -08:00
Nikolaj Bjorner
22fbed18cc fix regressions exposed by build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 11:18:52 -08:00
Christoph M. Wintersteiger
f093ebe44c Optimization for initialization of mpf's from tiny reals. 2016-01-12 19:06:53 +00:00
Nikolaj Bjorner
db746e0c2f fix more unused variable warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 09:52:16 -08:00
Nikolaj Bjorner
985fc50961 breaking regression tests: ensure that model values are of the sort of the original expression. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 09:48:43 -08:00
Nikolaj Bjorner
db71563478 fix build compiler warnings on OSX 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 09:36:01 -08:00
Nikolaj Bjorner
01c3e02e99 fix query for non-relational engines 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 07:57:10 -08:00
Mikolas Janota
613edfc107 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-12 13:19:29 +00:00
Christoph M. Wintersteiger
905fa56120 Merge pull request #414 from delcypher/typo_readme 
Fix minor typo in ``README.md``
 2016-01-12 12:28:18 +00:00
Dan Liew
55ea75d0a9 Fix minor typo in `README.md` 2016-01-12 11:25:30 +00:00
Nuno Lopes
08139d1ab1 fix build with gcc 2016-01-12 08:48:41 +00:00
Nikolaj Bjorner
f16550cf51 Merge pull request #413 from NikolajBjorner/master 
Multiple bug fixes  #405 #402 #399 #258 #354. Change Datalog "query" to use a function intead of an expression.
 2016-01-11 19:32:58 -08:00
Nikolaj Bjorner
78b93a5b95 Merge pull request #412 from delcypher/more_tidy_up_readme 
More tidy up readme
 2016-01-11 19:32:22 -08:00
Nikolaj Bjorner
3bf8b17b96 remove std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-11 19:22:11 -08:00
Nikolaj Bjorner
739c90779b Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-11 19:16:16 -08:00
Nikolaj Bjorner
e22ac712b0 add model construction for disequations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-11 16:53:29 -08:00
Dan Liew
7cc12bf59f Update information in `README.md` on Python bindings. Since 
e9ea687bb9 they aren't on by default.
Now ``--python`` needs to passed.

Also give better documentation on how install the Python bindings
outside the install prefix.
 2016-01-11 23:50:43 +00:00
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