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

2082 commits

Author SHA1 Message Date
Nikolaj Bjorner 03bd010b05 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 21:19:06 -07:00
Nikolaj Bjorner d67bfd78b9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 21:15:55 -07:00
Nikolaj Bjorner 40a79694ea add job/resource axioms on demand 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 16:33:34 -07:00
Nikolaj Bjorner 2839f64f0d rename to csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 11:05:55 -07:00
Nikolaj Bjorner 502c071266 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 09:57:06 -07:00
Nikolaj Bjorner d55fe1ac59 na' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-14 09:41:43 -07:00
Nikolaj Bjorner a096ec648c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-13 17:11:22 -07:00
Nikolaj Bjorner 540baa88f4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-13 17:08:34 -07:00
Nikolaj Bjorner 3478b8b924 add js-model interfacing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-12 18:14:06 -07:00
Nikolaj Bjorner 0af00e62de abstract arithmetic value extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-12 12:42:26 -07:00
Nikolaj Bjorner abd902d58c n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 18:14:32 -07:00
Nikolaj Bjorner 55f15b0921 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-10 17:52:34 -07:00
Nikolaj Bjorner baeff82e59 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-10 09:46:21 -07:00
Nikolaj Bjorner 0d8de8f65f add theory outlline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-09 20:19:26 -07:00
Nikolaj Bjorner f306f75e36 harness internalization and API for #1776 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 20:18:27 -07:00
Nikolaj Bjorner 8b08821112 fix #1784, fix #1783 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-01 17:31:14 -07:00
Nikolaj Bjorner 77d68409c2 handle null declarations for kind 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-01 08:43:32 -07:00
Nikolaj Bjorner 124e963b10 revert bit-resize issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 16:26:41 -07:00
Nikolaj Bjorner 4b00d6aef2 move mk-bits to mk-var 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 16:13:25 -07:00
Nikolaj Bjorner 22a5687e16 supply bits on demand 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-31 15:52:21 -07:00
Nikolaj Bjorner fdcedee887 hardening pop abuse and exception safety for #1776 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-30 09:56:16 -07:00
Nikolaj Bjorner 13390e2c3a fix #681, unsound propagation of binary equalities. Clean up memory leaks on exit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-29 12:08:59 -07:00
Nikolaj Bjorner 5509bf248a coallesce lambda/quant tracing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-29 08:02:56 -07:00
Nikolaj Bjorner 64e570f159 fix #1766 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-29 02:22:28 -07:00
Nikolaj Bjorner 1cb3f7c792 fixing #1520 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-28 18:03:13 -07:00
Nikolaj Bjorner d74978c277 fix #1762, #1764, #1768 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 20:29:26 +01:00
Nikolaj Bjorner 60bb02b709 updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-26 15:31:49 +01:00
Nikolaj Bjorner 30330c79a1 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-15 22:36:02 -07:00
Nikolaj Bjorner d00ffdda82 strengthen filter for specialized tactic conditions, add flag to disable hnf to lp_params 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-15 22:35:47 -07:00
Nikolaj Bjorner bdd8685146 use params for arguments to Fixedpoint methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 18:09:30 -07:00
Nikolaj Bjorner 88f4ce68fd fix model generation regression exposed in nightly builds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 13:51:07 -07:00
Nikolaj Bjorner 167969d6c2 remove debug/non-debug difference 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-13 07:52:36 -07:00
Nikolaj Bjorner f09f1a7524 Merge branch 'master' of https://github.com/z3prover/z3 2018-07-11 08:53:00 -07:00
Nikolaj Bjorner 3a5aebd1d3 tidy model generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-11 08:52:57 -07:00
Nikolaj Bjorner 9f2bafbf10 tidy model generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-11 08:52:13 -07:00
Nikolaj Bjorner e39107c682 turn lemma-id into an attribute on the cotext 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 21:26:51 -07:00
Nikolaj Bjorner 5e5f46f0f8 handle cancelation from nra_solver gracefully 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 17:34:45 -07:00
Nikolaj Bjorner 0170a9772a expose methods for dumping T-lemmas from theory_lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-10 16:44:48 -07:00
Nikolaj Bjorner fc4627a24f force the new arithmetic solver for QF_LIA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 16:33:48 -07:00
Nikolaj Bjorner 8373bec6ad only assign, if there isn't already a true literal incube/clause mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 10:33:56 -07:00
Nikolaj Bjorner efe440839e Merge branch 'master' of https://github.com/z3prover/z3 2018-07-09 09:19:37 -07:00
Nikolaj Bjorner 605dcc40a3 fix #1741 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-09 09:19:13 -07:00
Nikolaj Bjorner a2d078f6f5
Merge pull request #1737 from Nils-Becker/master 
Equality Explanation Logging
 2018-07-07 15:39:08 -07:00
Nikolaj Bjorner dfbd285dae avoid rewriting if reduces to tautology 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 22:02:48 -07:00
Nikolaj Bjorner 3ae0ea8246 add circuit and unate encoding besides sorting option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 21:09:13 -07:00
nilsbecker 820c14ed06 synchronize fork 2018-07-06 16:19:13 +02:00
nilsbecker a405742037 Adding comments 2018-07-06 12:43:46 +02:00
Nikolaj Bjorner 0b30ddb769 fix #1733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-06 02:09:47 -07:00
Lev Nachmanson 905282ffe4 fix in theory_lra.cpp get_value 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2018-07-05 14:47:05 -07:00
Nikolaj Bjorner c7e1d59b19 Merge branch 'master' of https://github.com/z3prover/z3 into lev 2018-07-03 13:42:50 -07:00