mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
5608 commits 23 branches 48 tags 157 MiB
Commit graph

5608 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
5069da62a3 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:45:06 -07:00
Nikolaj Bjorner
e132c5eae8 safe sat clause_offset in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-19 08:42:40 -07:00
Nikolaj Bjorner
b2383a481a Merge branch 'master' of https://github.com/Z3Prover/z3 2016-08-18 18:02:22 -07:00
Nikolaj Bjorner
665fccf07a addressing max-segment issue for AMD64 + Debug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-18 18:01:29 -07:00
Christoph M. Wintersteiger
e8141aaa84 debug fixes 2016-08-12 19:52:59 +01:00
Christoph M. Wintersteiger
244c641234 debug check fix 2016-08-12 13:19:12 +01:00
Christoph M. Wintersteiger
b74bff7fb7 logic detection fix 2016-08-10 11:39:47 +01:00
Christoph M. Wintersteiger
f54a7db108 Added debug traces. 2016-08-09 16:36:49 +01:00
Christoph M. Wintersteiger
ff3c630207 .NET API: Added MkMul from IEnumerable. 2016-08-09 16:36:32 +01:00
Christoph M. Wintersteiger
03aa6914a3 Fixed sub-logic detection for the ALL logic. 2016-08-09 13:20:45 +01:00
Nikolaj Bjorner
aee6a7fe4c Merge pull request #708 from dstaple/master 
Removed complete() from handling of y.is_zero() in process_power
 2016-08-06 09:06:34 -07:00
Nikolaj Bjorner
14e8126f16 wrapping interruptable with solver consequence call 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-05 11:32:12 -07:00
Douglas B. Staple
87b7674245 Removed complete() from handling of y.is_zero() in process_power 2016-08-05 14:11:51 -03:00
Nikolaj Bjorner
f3ef59b095 fix scanner bug at EOF 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-04 13:17:37 -07:00
Nikolaj Bjorner
491b3b34aa tune consequence finding. Factor solver pretty-printing as SMT-LIB into top-level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-08-03 11:14:29 -07:00
Nikolaj Bjorner
cb2d8d2107 add detection of non-fixed variables to consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 19:12:41 -07:00
Nikolaj Bjorner
7562efbe84 add consequence command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 12:59:29 -07:00
Nikolaj Bjorner
7346098895 fix unsat core extraction code in smt_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 11:22:34 -07:00
Nikolaj Bjorner
d32019f4c9 fix consequence tracking for negated assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-30 10:49:06 -07:00
Nikolaj Bjorner
7d545d902d switch to specialized consequence generator in combined_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:36:11 -07:00
Nikolaj Bjorner
2263be1b4d adding consequence examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-29 17:24:14 -07:00
Nikolaj Bjorner
82d0310d94 remove repeated default argument, remove tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 21:13:12 -07:00
Nikolaj Bjorner
5c99405db3 finish consequence fast path code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 20:15:47 -07:00
Nikolaj Bjorner
4958edeb42 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 19:40:49 -07:00
Nikolaj Bjorner
fa48703445 fix build for non C++11 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 17:04:47 -07:00
Nikolaj Bjorner
0055254f4c fix build for non C++11 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 17:04:06 -07:00
Christoph M. Wintersteiger
2e362aa6c0 build fix 2016-07-29 01:02:48 +01:00
Nikolaj Bjorner
46c911a92f Merge pull request #700 from lorisdanto/master 
added symbolic automata complement for sequences
 2016-07-28 17:00:23 -07:00
Christoph M. Wintersteiger
6e85c5e987 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-29 00:55:22 +01:00
Christoph M. Wintersteiger
7fd931d480 build fix 2016-07-29 00:55:05 +01:00
Nikolaj Bjorner
55cffc5247 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 16:49:49 -07:00
Nikolaj Bjorner
8221a09659 fast path for antecedent extraction in smt_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 16:49:19 -07:00
Loris D'Antoni
73bd4acfc5 added symbolic automata complement for sequences 2016-07-28 13:50:05 -07:00
Christoph M. Wintersteiger
5f449b5c0d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 19:52:56 +01:00
Nikolaj Bjorner
ceb3f0c869 patch full version for cmake to re-enable build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:30:39 -07:00
Nikolaj Bjorner
074f1ad778 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 11:20:23 -07:00
Nikolaj Bjorner
14f29e7265 add basic built-in consequence finding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-28 11:20:17 -07:00
Christoph M. Wintersteiger
d5954e829b Enabled donet key file in dist scripts 2016-07-28 18:49:57 +01:00
Christoph M. Wintersteiger
6f874c5c1d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-28 18:07:48 +01:00
Christoph M. Wintersteiger
7fefe40f21 Added/improved facilities for strong name signing of the .NET assembly. 2016-07-28 18:07:34 +01:00
Christoph M. Wintersteiger
0d83f99d8d Fixed comment 2016-07-28 18:06:26 +01:00
Christoph M. Wintersteiger
3587baaf24 Added full version strings and associated API functions. 2016-07-28 18:06:02 +01:00
Nikolaj Bjorner
b7de813c63 set solver on simplify command 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 15:35:44 -07:00
Nikolaj Bjorner
0997eba700 adding hash/eq to uint_set 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 13:41:41 -07:00
Nikolaj Bjorner
1239c8f8e8 update MSF example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 11:20:31 -07:00
Nikolaj Bjorner
5f5ef8b38d adding support for distinct for dt2bv, re-entry harness for ~Context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-27 09:02:56 -07:00
Nikolaj Bjorner
375682e98d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-26 14:31:40 -07:00
Nikolaj Bjorner
9cab896632 adding sign option if keyfile is present 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-07-26 14:31:29 -07:00
Christoph M. Wintersteiger
8fa29f6970 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-07-26 19:21:57 +01:00
Christoph M. Wintersteiger
eec68cfa2d Added 32/64 bit indication and githash to output of -version. 2016-07-26 19:21:50 +01:00