3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-09 10:51:50 +00:00
Commit graph

4694 commits

Author SHA1 Message Date
Mikolas Janota e7477e2f6a Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:51 +00:00
Mikolas Janota 0dc8dc4d8e Moving things around. Adding tactic just for ackermannization. 2016-01-26 17:02:30 +00:00
Mikolas Janota 470f8bca73 Merge remote-tracking branch 'upstream/master' into lackr 2016-01-26 16:51:57 +00:00
Mikolas Janota c63f9f4912 Moving things around. Adding tactic just for ackermannization. 2016-01-26 16:50:00 +00:00
Nikolaj Bjorner 8e378062e2 add get-some-value to seq API, expose quantifier tactics
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-26 08:05:44 -08:00
Nikolaj Bjorner 345f6e87bd seq bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-26 07:21:31 -08:00
Mikolas Janota 3978410fcb Merge branch 'lackr' of github.com:MikolasJanota/z3 into lackr 2016-01-26 14:23:50 +00:00
mikolas d32c9449b2 Editing some comments and also enabling to export the ackermannized formula as a gole. 2016-01-26 11:53:47 +00:00
Mikolas Janota c2edf2c5bf Merge remote-tracking branch 'upstream/master' into lackr 2016-01-25 13:04:46 +00:00
Nikolaj Bjorner 924f03c6de fixing bugs in seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-23 10:38:49 -05:00
Nikolaj Bjorner 993a0434b4 fix warning message for unused variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-19 23:47:35 -05:00
Nikolaj Bjorner 099e572a26 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-19 19:10:08 +01:00
Nikolaj Bjorner a021e51a9c make parse error a bit more informative
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-19 19:09:41 +01:00
Nuno Lopes 23cc8258fe remove m_ast_lim from API context since that one isn't used either
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2016-01-19 15:37:58 +00:00
Nuno Lopes 1f872e720d remove m_replay_stack from API context since it's never used
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2016-01-19 15:19:00 +00:00
Nikolaj Bjorner d9e4648d8d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-19 13:57:59 +01:00
Nikolaj Bjorner cccd502a4d bug-fixes to sequence theory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-19 13:57:47 +01:00
Christoph M. Wintersteiger 4dba5270ad Efficiency fix for fp.div. 2016-01-18 18:09:29 +00:00
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