mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
6814 commits 49 branches 53 tags 182 MiB
Commit graph

1446 commits

Author SHA1 Message Date
Nikolaj Bjorner
67397bf71e enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:48:24 -08:00
Nikolaj Bjorner
7f51ecab37 enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:26:14 -08:00
Nikolaj Bjorner
908f09a9df update logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 08:46:43 -08:00
Nikolaj Bjorner
df2d7e7628 add intersection using symbolic automata facility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-28 17:05:12 -08:00
Nikolaj Bjorner
e659845bc0 tune handling of contains, avoid redundant equalities, merge use of indexof.left/right with contains.left/right adding only least-ness constraints in the context of index 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-27 09:56:11 -08:00
Nikolaj Bjorner
1c630ccc9a Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2016-02-26 18:15:57 -08:00
Nikolaj Bjorner
ce8862d415 fix bug in conflict clause generation in seq-branch-variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-26 18:15:45 -08:00
Nuno Lopes
d642d5fe4c API: add smt.logic parameter to enable setting the logic through the API 
currently only Z3_solver_set_params() is supported
logic has to be set before solver first usage or before solver reset
 2016-02-25 09:47:51 +00:00
Nikolaj Bjorner
4c408165ab Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2016-02-24 08:55:28 -08:00
Nikolaj Bjorner
5679fb5d6b experimenting with alternative prefix encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-24 08:55:22 -08:00
Nikolaj Bjorner
d5383e2387 fix bug in definition of rewrite rule for replace, tighten constraints for tightest-prefix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-23 18:41:56 -08:00
Nikolaj Bjorner
c7abc11ce0 Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2016-02-19 08:23:32 -08:00
Nikolaj Bjorner
bff10527d1 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-19 08:23:27 -08:00
Nikolaj Bjorner
a073b37ce3 fix bugs in seq solver: add relevancy and axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-18 18:10:16 -08:00
Nikolaj Bjorner
5962ca2a62 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-18 12:08:35 -08:00
Nikolaj Bjorner
67958efed2 add fixed length heuristic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-17 21:20:39 -08:00
Nikolaj Bjorner
a6e1c70eab fix documentation/default bug. #445 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-10 15:02:22 +00:00
Dan Liew
ea900db337 Explicitly state what the units of the timeout parameter for the "smt" 
module are.
 2016-02-10 11:35:15 +00:00
Nikolaj Bjorner
60c0e73b2f Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-09 11:08:52 +00:00
Nikolaj Bjorner
133e3693de fix bug in replace built-in and move length-equality propagation to branch final check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-09 11:08:33 +00:00
Christoph M. Wintersteiger
a2f376f9d6 Fixed memory leak in theory_fpa. Relates to #436 2016-02-08 17:17:49 +00:00
Nikolaj Bjorner
677b4bf4fe fix #436, adding more length-based propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-07 14:43:53 +00:00
Nikolaj Bjorner
5b50d98b89 ensure that seq rewriter gets invoked during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-06 16:13:31 +00:00
Nikolaj Bjorner
2a65503235 fix #425 and report from Patrick Trentin of same bug in preprocessing soft constraints that are simplified to true/false 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 22:35:02 +00:00
Nikolaj Bjorner
768bb84798 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-04 08:12:56 -08:00
Nikolaj Bjorner
9c7e5c37d1 add equality propagation based on partial length information to sequence theory. Fix issue #429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 08:12:46 -08:00
Christoph M. Wintersteiger
4e37821dde "canceled" -> Z3_CANCELED_MSG 
Relates to #431
 2016-02-04 13:52:43 +00:00
Nikolaj Bjorner
9b979b6e1e more string optimizations based on Chris' examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-01 17:08:11 -08:00
Nuno Lopes
b9c0578eea fix build on C++98 compilers 2016-02-01 17:12:22 +00:00
Nikolaj Bjorner
995a2e1a29 perf tuning based on Chris's examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-01 07:51:05 -08:00
Nikolaj Bjorner
2115111dac update display method for datalog to use predicates, throttle use of extensionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 20:23:06 -08:00
Nikolaj Bjorner
30f8110488 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:51:04 -08:00
Nikolaj Bjorner
b352d43e50 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:50:13 -08:00
Nikolaj Bjorner
6529d43fb1 fix bugs exposed by unit tests from Pierre 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 09:50:14 -08:00
Nikolaj Bjorner
345f6e87bd seq bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 07:21:31 -08: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
cccd502a4d bug-fixes to sequence theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 13:57:47 +01: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
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
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
Christoph M. Wintersteiger
0f082578cb Debug-fix for theory_seq. Fixes #418. 2016-01-14 13:07:48 +00: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
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
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
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