mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-04 14:25:46 +00:00
Code Activity
7620 commits 25 branches 48 tags 158 MiB
Commit graph

7620 commits

This branch
This branch
All branches
Author SHA1 Message Date
Christoph M. Wintersteiger
4857de6c81 fixed buggy if condition 2015-10-04 15:16:03 +01:00
Zachary Kincaid
9e34872e8f For ocamlfind install, set rpath to package directory if stublibs does not exist 2015-10-04 10:10:53 -04:00
Nikolaj Bjorner
459e456f66 disable memory finalization after quant_solve unit test. Related to issue #210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:37:33 -07:00
Nikolaj Bjorner
62a4737d77 disable code in dl_query that depends on hard-wired file path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:30:12 -07:00
Nikolaj Bjorner
50993582ec put break statement in else branh. Issue #230 (broken loop) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:15:54 -07:00
Nikolaj Bjorner
89f1541d83 put break statement in else branh. Issue #230 (broken loop) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-03 17:15:45 -07:00
Murphy Berzish
6791db64c0 process_concat_eq_type6 
that's the last one!
 2015-10-03 13:34:42 -04:00
Murphy Berzish
be79723382 process_concat_eq_type5 wip 2015-10-03 12:26:30 -04:00
Murphy Berzish
f7bc785a56 process_concat_eq_type4, still WIP not tested 2015-10-03 12:19:55 -04:00
Murphy Berzish
ff4706dd40 process_concat_eq_type3 
still wip because i'm just trying to get these all done
 2015-10-03 12:07:55 -04:00
Christoph M. Wintersteiger
bcd3f56fa0 Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-03 16:25:47 +01:00
Christoph M. Wintersteiger
d8524ae4dd Fixed indentation 2015-10-03 16:24:06 +01:00
Christoph M. Wintersteiger
215f9d26eb Updated release notes 2015-10-02 20:07:42 +01:00
Christoph M. Wintersteiger
2397f37def Merge branch 'pure' of https://github.com/Z3Prover/z3 2015-10-02 19:55:22 +01:00
Christoph M. Wintersteiger
114f9834dd Adjusted copyright notice. 2015-10-02 19:51:06 +01:00
Christoph M. Wintersteiger
3b81118f4a Merge branch 'contrib' of https://github.com/Z3Prover/z3 2015-10-02 19:47:49 +01:00
Christoph M. Wintersteiger
95dea3922d Merge branch 'pure' of https://github.com/Z3Prover/z3 
Conflicts:
	src/api/ml/z3.ml
	src/api/ml/z3.mli
	src/api/python/z3util.py
 2015-10-02 19:47:24 +01:00
Christoph M. Wintersteiger
a9d395ed7a Fixed comments about contributed code. 2015-10-02 19:45:33 +01:00
Murphy Berzish
96d99dfb38 process_concat_eq_type2 implementation, not tested WIP 2015-10-02 14:05:17 -04:00
Christoph M. Wintersteiger
18a0314f6b Fix for ast_map in ML API 2015-10-02 15:52:33 +01:00
Christoph M. Wintersteiger
e0026a1cbb Merge branch 'contrib' of https://github.com/Z3Prover/z3 2015-10-02 15:20:06 +01:00
Christoph M. Wintersteiger
0a95df8960 removed automatically generated file 2015-10-02 15:11:53 +01:00
Christoph M. Wintersteiger
08a3ab92f3 Added --noomp to mk_make 2015-10-02 12:38:56 +01:00
Murphy Berzish
bdf755156c fix model generation: don't build interpretations for Length() 2015-10-01 20:31:40 -04:00
Christoph M. Wintersteiger
1294a2ac15 Fixed a memory leak 2015-10-01 13:31:37 +01:00
Murphy Berzish
fb5f3cbc13 fix greater-than bug 
now we just have to tweak model gen for internal variables
 2015-09-30 11:41:55 -04:00
Murphy Berzish
f8c13792a3 mark the position of the bug I found so I can recall it later 
in process_concat_eq_type1() line 1048
 2015-09-30 09:45:00 -04:00
Murphy Berzish
5189c24d42 fix theory of arithmetic complaints about wanting to write A > B 
"what could possibly go wrong?"
 2015-09-30 05:45:16 -04:00
Murphy Berzish
ecb2116927 fix memory corruption bug caused by invalid use of delete[] 2015-09-30 05:23:22 -04:00
Murphy Berzish
e2901fff1e fix compilation errors 2015-09-30 05:21:16 -04:00
Murphy Berzish
ed7b343822 detect and process concat eq type 1 (WIP UNTESTED) 2015-09-30 05:15:14 -04:00
Murphy Berzish
a62d15403e start simplify_concat_eq(), WIP but some cases OK 
also fix model generation for concats and nested concats
 2015-09-29 22:31:11 -04:00
Murphy Berzish
1cdfe159b8 simplify_concat_equality() and easy cases there 
still WIP especially wrt. model generation but what's here does work
 2015-09-29 20:19:43 -04:00
Nikolaj Bjorner
5d71190468 add catch for cancellation intermixed with return value l_true. To address regressions in QF_LIA tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 16:50:59 -07:00
Murphy Berzish
8ed86d2f19 add concatenation axiom 2015-09-29 18:02:05 -04:00
Murphy Berzish
191c50b529 fix solve_concat_eq_str() case 4: prefixStr should have been suffixStr 2015-09-29 17:52:19 -04:00
Murphy Berzish
2320b6dc48 solve_concat_eq_str() case 4: somewhat working 
something's wrong but it may be very simple to fix
 2015-09-29 17:46:51 -04:00
Nikolaj Bjorner
77c423b9aa annotate enode hash as signed character to address issue #210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 14:14:29 -07:00
Nikolaj Bjorner
074ff58739 include rlimit in nlsat, include dedicated error message, for issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 09:27:34 -07:00
Nikolaj Bjorner
d9b6623400 include rlimit in nlsat, include dedicated error message, for issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-29 09:16:46 -07:00
Christoph M. Wintersteiger
0cf18ab18e Propagated rlimit changes to sat::solver into sat_user_scope tests 2015-09-29 11:50:10 +01:00
Murphy Berzish
f473b92d5c solve_concat_eq_str() case 4 WIP 2015-09-28 17:41:01 -04:00
Nikolaj Bjorner
1f9d5249a3 fix build break regarind z3test.py and added rlimit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 14:05:57 -07:00
Nikolaj Bjorner
f3b8fe130a adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities. This is to address issue #216 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:40:54 -07:00
Nikolaj Bjorner
9b3e242990 adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 13:37:59 -07:00
Murphy Berzish
871b08bd8c solve_concat_eq_str() case 3 2015-09-28 14:52:43 -04:00
Murphy Berzish
876af399e3 probably fix duplication of mk_string() terms 
also implement Case 2 of solve_concat_eq_str()
 2015-09-28 14:44:25 -04:00
Nikolaj Bjorner
ad16cc0ce2 fix unit test for datalog parser, fixes issue #224 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-28 11:16:55 -07:00
Christoph M. Wintersteiger
ac7e8b352f Improved support for UFs in FPA theory 2015-09-28 18:20:45 +01:00
Christoph M. Wintersteiger
de3ead9ff1 build fix 2015-09-28 18:20:22 +01:00