mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity
5619 commits 24 branches 48 tags 158 MiB
Commit graph

4572 commits

Author SHA1 Message Date
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
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
0d54e4e4ae implement str_decl_plugin::is_value() and ::is_unique_value() 
we can now prove that (= "abc" "def") is unsatisfiable
 2015-09-27 23:57:41 -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
2744d80642 Fixed reference counting in fpa2bv converter. 2015-09-23 14:22:02 +01:00
Christoph M. Wintersteiger
04266fccc9 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 20:56:07 +01:00
Christoph M. Wintersteiger
0b15fc9402 Bugfix for mpf sqrt. 
Fixes #222.
 2015-09-21 19:44:53 +01:00
Christoph M. Wintersteiger
d4b66538f9 Bug/assertion fix for power monomials in nlsat. 
Previously triggered an assertion on regressions/smt2/fp-to_real-1.smt2, but only on OSX and FreeBSD
 2015-09-17 16:31:51 +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
Christoph M. Wintersteiger
d2c9b69eb3 fixed memory leak (`mem' remained allocated upon exception thrown in check_args). 2015-09-17 13:20:24 +01:00
Christoph M. Wintersteiger
2e071e89b0 tabs 2015-09-17 13:16:35 +01:00
Christoph M. Wintersteiger
4d39108808 Bugfix for fp.to_sbv 
Fixes #162
 2015-09-17 12:21:59 +01:00
Christoph M. Wintersteiger
e9565d6a7f Fixed warning message 2015-09-17 12:18:44 +01:00
Christoph M. Wintersteiger
2115ea8bb8 Bugfix for fp.sqrt. 
Fixes #220.
 2015-09-17 12:13:04 +01:00
Christoph M. Wintersteiger
52df2224e9 Disabled FP debug variables. 2015-09-16 18:04:26 +01:00
Christoph M. Wintersteiger
27f8ad288c Bugfix for fp.to_ubv. 
Fixes #162.,
 2015-09-16 14:26:53 +01:00
Christoph M. Wintersteiger
79d69cd5f0 Added FP to_ieee_bv to fpa_rewriter to enable model evaluation. 2015-09-16 12:57:05 +01:00
Christoph M. Wintersteiger
46e24e094c fixed warning message 2015-09-16 12:08:56 +01:00
Christoph M. Wintersteiger
869cd6074d Bugfix for fp.to_sbv and fp.to_ubv. 
Fixes #162.
 2015-09-15 19:03:31 +01:00
Christoph M. Wintersteiger
a1073206f9 Bugfix for FP rewriter. 2015-09-15 16:23:24 +01:00