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

2076 commits

Author SHA1 Message Date
Nikolaj Bjorner
6e852762ba patch for issue #232 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-06 19:07:47 -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
Murphy Berzish
96d99dfb38 process_concat_eq_type2 implementation, not tested WIP 2015-10-02 14:05:17 -04:00
Murphy Berzish
bdf755156c fix model generation: don't build interpretations for Length() 2015-10-01 20:31:40 -04: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
Murphy Berzish
f473b92d5c solve_concat_eq_str() case 4 WIP 2015-09-28 17:41:01 -04: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
Christoph M. Wintersteiger
ac7e8b352f Improved support for UFs in FPA theory 2015-09-28 18:20:45 +01:00
Murphy Berzish
9bc685b21d solve_concat_eq_str() for concat(const,const) == const 2015-09-28 10:43:34 -04:00
Murphy Berzish
62cd633b63 create helper function theory_str::assert_implication() 2015-09-28 03:26:46 -04:00
Murphy Berzish
bccadedfee instead of building axiom (=> x y), build (or (not x) y) 
this may be a bug in Z3 as it suggests that implications are ignored
e.g. I can assert the axiom (=> true false) and Z3 is okay with this
 2015-09-28 03:20:13 -04:00
Murphy Berzish
5fe129b571 use mk_ismt2_pp() instead of mk_bounded_pp() 2015-09-28 02:09:35 -04:00
Murphy Berzish
87b5765e3d clean up traces and make them much easier to read 2015-09-28 02:04:35 -04:00
Murphy Berzish
7da3854a8b really lousy model-building, WIP 2015-09-28 01:56:13 -04:00
Murphy Berzish
02cb329ca5 defer equalities uncovered during init_search 2015-09-27 23:24:41 -04:00
Murphy Berzish
86e6087718 starting solve_concat_eq_str(); currently there is an unsoundness bug 2015-09-27 21:30:45 -04:00
Murphy Berzish
6481fe941a instantiate string-eq length-eq axiom 2015-09-27 17:48:53 -04:00
Murphy Berzish
114b51dec8 only handle equalities in assignments during init_search_eh 2015-09-27 17:26:52 -04:00
Murphy Berzish
91e9cf272a assert string axiom 2 2015-09-27 00:12:04 -04:00
Murphy Berzish
4085db9990 recursive descent through all assertions to discover all String terms 
set up axioms on these terms to be asserted during propagation
 2015-09-26 23:35:23 -04:00
Murphy Berzish
f6affe64d0 deferred addition of basic string axioms 
no longer crashes the solver and got our first correct UNSAT!
 2015-09-26 21:02:56 -04:00
Murphy Berzish
4d5a0ea53f WIP add axioms 2015-09-26 18:51:02 -04:00
Christoph M. Wintersteiger
076e680433 Improved UF suppport in fpa2bv_converter. 2015-09-25 17:28:31 +01:00
Christoph M. Wintersteiger
05d9e188f8 Reactivated smt.max_conflicts option. 
Partially fixes #216.
 2015-09-17 14:08:04 +01:00
Christoph M. Wintersteiger
f3441c6a9b tabs and indentation 2015-09-17 13:25:22 +01:00
Nuno Lopes
45cfb80d14 tentatively fix another issue with char signedness as reported in issue #210 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-09-10 09:01:44 +01:00
Nikolaj Bjorner
d7da64f946 fix crash with incorrect bound computation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-08 16:27:57 -07:00
Nikolaj Bjorner
73a8f9960f fix regressions exposed in Internal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-07 20:17:46 -07:00
Murphy Berzish
799fd07c85 optimization: return integer consts for strlen() over constant strings 2015-09-07 19:51:52 -04:00
Murphy Berzish
9b04f1570f instantiate length axiom for concatenation 2015-09-07 19:40:25 -04:00
Murphy Berzish
dc86385e7f add Length function to theory of strings 2015-09-07 16:13:48 -04:00
Murphy Berzish
8137e022e3 load str decl plugin; recognize String sorted constants 2015-09-06 20:53:08 -04:00
Nikolaj Bjorner
963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-08-31 14:45:10 -07:00