mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 07:15:47 +00:00
Code Activity
7098 commits 25 branches 48 tags 158 MiB
Commit graph

5762 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
406cd00b3a Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-15 10:54:17 +02:00
Nikolaj Bjorner
f94152c857 fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-15 10:54:01 +02:00
Christoph M. Wintersteiger
d6e2fa6a60 Bugfix for MPF fma. 2015-09-14 14:07:11 +01:00
Christoph M. Wintersteiger
d0fa4e992f Bugfix for fp.to_sbv. 
Fixes #162
 2015-09-14 14:04:31 +01:00
Nikolaj Bjorner
b25e8e2288 tune lexicographic products, avoid push/pop and ensure correction sets are not used for multiple objectives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-13 16:00:45 +02:00
Guang Chen
cef7ec2157 fix implies(expr const &, expr const &) in z3++.h 2015-09-13 13:29:06 +08:00
Nikolaj Bjorner
e3840a7fc6 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-12 14:47:49 +02:00
Nikolaj Bjorner
a8b47b4fb2 enable coercions when interpolation creates MILP constraints. Issue #217 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-09-12 14:47:35 +02:00
Murphy Berzish
992fff8ba8 set up theory of arithmetic correctly 
closes #1
 2015-09-10 18:43:14 -04:00
Christoph M. Wintersteiger
646dcfb6e6 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-09-10 11:37:18 +01:00