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

5192 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger 99176cca60 Bugfix for FP model converter. 2016-01-18 18:00:04 +00:00
Nikolaj Bjorner c9373ebc9f fix axiomatization for at 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-18 12:01:15 +05:30
Nikolaj Bjorner 6aed3c3a44 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-18 11:09:52 +05:30
Nikolaj Bjorner 85d44c5d66 fix axioms for extract, add extensionality checking for shared variables, convert exceptions to unknown status per #419 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-18 11:09:41 +05:30
Christoph M. Wintersteiger 99d2ab4e8e Undid previous update of SMT2 scanner to support the new SMT2.5 string escaping. 2016-01-17 14:24:02 +00:00
Christoph M. Wintersteiger 01cb20e098 Fix for escape sequences in SMT2 scanner 2016-01-16 13:53:29 +00:00
Nikolaj Bjorner 88362a1c3a fix bugs in sequence extraction from NFA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 16:32:43 +05:30
Nikolaj Bjorner 14c19fe928 add parameter validation to sequence expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 10:39:21 +05:30
Nikolaj Bjorner 150c5c283d update re simplification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 10:11:39 +05:30
Nikolaj Bjorner a295dd48dc add seq_rewriter to model_evaluator, remove th_rewriter additional step in validator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 04:02:48 +05:30
Nikolaj Bjorner 7cbd59bf06 enhance model validation to invoke rewriter if result isn't true using the simplify-based model evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 03:40:33 +05:30
Nikolaj Bjorner 01fd3c919b fix tout -> out. Tune generation of automata transitions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 03:32:27 +05:30
Nikolaj Bjorner 2d41b0e29b fix tout -> out. Tune generation of automata transitions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-15 03:31:30 +05:30
Mikolas Janota c6df8b3128 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-14 15:25:04 +00:00
Mikolas Janota 7ec13166b1 Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-14 14:21:28 +00:00
mikolas d97e2b432c Ackermann run on separate assertions rather than an AND thereof. 2016-01-14 14:11:11 +00:00
Christoph M. Wintersteiger 0f082578cb Debug-fix for theory_seq. Fixes #418. 2016-01-14 13:07:48 +00:00
Nikolaj Bjorner 3ff97357a3 fix back rewriting for concat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-14 11:22:11 +01:00
Nikolaj Bjorner de9c959241 add support for re.nostr, re.all, fix bug in disequality handling of sequences, update signature of loop to handle integer arguments and variable arguments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-14 10:56:03 +01:00
Nikolaj Bjorner a81c7c48d0 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-14 00:56:52 +01:00
Nikolaj Bjorner 2f0a049df8 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-13 20:13:29 +01:00
Nikolaj Bjorner e0215400e2 add empty/full regular languages, escape sequence fixes, check cancellation inside simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-13 20:13:17 +01:00
Mikolas Janota a5ea17f1e3 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-13 18:22:58 +00:00
Christoph M. Wintersteiger 357ec9e7d1 Changed FP significand/exponent functions to return non-normalized results. Clarified function remarks. Relates to #383. 2016-01-13 16:32:32 +00:00
Mikolas Janota 094d357b07 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-13 12:10:36 +00:00
Christoph M. Wintersteiger e0f873c732 Merge pull request #409 from delcypher/ml_respect_destdir 
Respect DESTDIR when installing OCaml bindings
 2016-01-13 11:31:46 +00:00
Nikolaj Bjorner 57e1d4dc1f model generation with strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-13 10:39:38 +01:00
Nikolaj Bjorner 9909c056f0 add range / loop handling for re. Fix regression reading mixed numerals reported by Trentin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-13 00:49:31 -08:00
Nikolaj Bjorner 9a6fe93e6c re-enable feature that lets Z3 solver mixed integer/real constraints with additional information tha texpressions with sort real can only take integer values. Fixes regression on epsilon.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-12 12:42:18 -08:00
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