mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity
4860 commits 24 branches 48 tags 158 MiB
Commit graph

3970 commits

Author SHA1 Message Date
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
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
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
Nuno Lopes
08139d1ab1 fix build with gcc 2016-01-12 08:48:41 +00: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
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