mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
6306 commits 49 branches 53 tags 182 MiB
Commit graph

5070 commits

Author SHA1 Message Date
Nikolaj Bjorner
8ba78081ec fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 16:41:17 -07:00
Nikolaj Bjorner
61e0fc9099 Merge pull request #995 from mtrberzi/theory-case-split 
Theory case split heuristic (for theory_str)
 2017-05-01 15:27:45 -07:00
Murphy Berzish
16a5e944d7 use reference for case split sets 2017-05-01 18:25:54 -04:00
Nikolaj Bjorner
f9105edb14 revert to native chunker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:52 -07:00
Murphy Berzish
b86d472eaf simplify theory case split handling 2017-05-01 18:22:49 -04:00
Nikolaj Bjorner
d14f2af5ae deal with subtraction that manages to sneak in. Issue #996 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:06 -07:00
Murphy Berzish
3bce61e0d4 fix warning 2017-05-01 10:43:33 -04:00
Murphy Berzish
2f56d128b0 add theory case split support to smt_context 2017-05-01 10:34:43 -04:00
Murphy Berzish
f655e1976e add params for theory case split 2017-05-01 10:18:38 -04:00
Nikolaj Bjorner
aceee3fac8 renmae to opt_stream_buffer to avoid clash with dimacs stream buffer. #994 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 12:54:29 -07:00
Nikolaj Bjorner
0693a413b6 augment #955 to handle hyphen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 12:50:56 -07:00
Nikolaj Bjorner
86f3526110 update get-value to also respect parameter model_index, #955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 11:48:06 -07:00
Nikolaj Bjorner
d6e2e1f28f Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 11:28:26 -07:00
Nikolaj Bjorner
aff02ca905 include 'stopwatch.h' to avoid ODR warnings, #994 2017-04-30 11:28:11 -07:00
Nikolaj Bjorner
bd1b930d7a swap argument order of chunk with file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 11:00:03 -07:00
Nikolaj Bjorner
5fcbf55216 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 10:23:05 -07:00
Nikolaj Bjorner
2c208e1d10 Sat update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 10:23:00 -07:00
Nikolaj Bjorner
4468816d32 fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 19:00:15 -07:00
Nikolaj Bjorner
b3f720c2bf fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 18:58:34 -07:00
Nikolaj Bjorner
3152833893 fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 18:55:47 -07:00
Nikolaj Bjorner
944dfbc6ef Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-29 17:39:20 -07:00
Nikolaj Bjorner
fa868e058e fix bound bug #991 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 17:39:02 -07:00
Murphy Berzish
88147f7047 theory_str static features and cmd_context 2017-04-28 14:14:28 -04:00
Nikolaj Bjorner
62a36189d5 Merge pull request #988 from mtrberzi/theory_str-frontend 
Frontend changes for theory_str
 2017-04-28 08:21:18 -07:00
Murphy Berzish
05958193ab revert change to String sort declaration 2017-04-27 22:30:02 -04:00
Murphy Berzish
12dd6d786b remove redundant is_seq() check 2017-04-27 21:24:40 -04:00
Murphy Berzish
7811a91bad fix is_string_term() 2017-04-27 13:59:02 -04:00
Nikolaj Bjorner
69aa5ca877 Merge pull request #984 from delcypher/cmake_doxygen 
[CMake][Doxygen] Support building/installing API documentation and fix lots of bugs
 2017-04-27 06:58:32 -07:00
Nikolaj Bjorner
d3b30968fa added chunk based backbone utility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-26 16:55:56 -07:00
Murphy Berzish
46ac718790 theory_str frontend changes 2017-04-26 17:24:05 -04:00
Nikolaj Bjorner
a048d74bae adding interval designator to output of non-optimal objectives, fix python doc test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-26 14:05:33 -07:00
Nikolaj Bjorner
8032217fd1 tuning and fixing consequence finding, adding dimacs evaluation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-26 13:53:37 -07:00
Dan Liew
fe702d7782 [Doxygen] Fix warning about non-existent functions. 
`Z3_push` and `Z3_pop` should be `Z3_solver_push` and `Z3_solver_pop`
respectively.
 2017-04-26 10:42:57 +01:00
Dan Liew
7242a77a3f [Doxygen] Fix typo found with Doxygen warning 
```
warning: Found unknown command `\s'
```
 2017-04-26 10:42:57 +01:00
Dan Liew
eb1c985a94 [Doxygen] Fixed malformed code blocks in z3_api.h. 
These malformed `\code` blocks caused broken documentation to
be generated.
 2017-04-26 10:42:57 +01:00
Nikolaj Bjorner
dedc130e98 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-25 10:30:16 -07:00
Nikolaj Bjorner
bd8b0186d6 make SMT consequence finding work with compound terms and formulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-25 10:30:10 -07:00
Nikolaj Bjorner
48b62d34b7 make sure consequence generation works with interpreted atoms/terms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-24 18:08:52 -07:00
Nikolaj Bjorner
34acaa8f56 update license for space/quotes per #982 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-24 13:34:10 -07:00
Bruce Collie
ce67c8277c Return check result in fixedpoint object 
This is a small change to fix a missing return statement.
 2017-04-24 12:59:44 +00:00
Nikolaj Bjorner
5068d2083d tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-22 11:36:03 -07:00
Murphy Berzish
367cc4b77f check result of unsat core validation 2017-04-22 13:36:09 -04:00
Murphy Berzish
a1bb1f2a13 pre-init assumptions and unsat core validation for smt theories 2017-04-22 13:15:00 -04:00
Christoph M. Wintersteiger
0a0b17540f Added rlimit.inc() for expensive interval exponentiation in the non-linear arithmetic theory. 2017-04-19 13:07:04 +01:00
Christoph M. Wintersteiger
a02a7f4443 Whitespace 2017-04-19 13:04:04 +01:00
Christoph M. Wintersteiger
71da36f85c Added core.extend_nonlocal_patterns parameter to improve unsat cores. 2017-04-18 15:13:11 +01:00
Nikolaj Bjorner
66e61b8a31 issues #963 #912 2017-04-17 03:06:38 -07:00
Nikolaj Bjorner
8b5627e361 additional API per #977 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-16 12:13:30 +09:00
Nikolaj Bjorner
9933c36050 replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 17:06:03 +08:00
Nikolaj Bjorner
ab6abe901f replace long by int 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-15 15:57:30 +08:00