mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity
7500 commits 24 branches 48 tags 158 MiB
Commit graph

6121 commits

Author SHA1 Message Date
Murphy Berzish
fce35fdb61 Revert "fix indentation and add support for re.allchar" 
This reverts commit cadde94017.
 2017-08-09 15:37:52 -04:00
Nikolaj Bjorner
082936bca6 enable overloading resolution on define-fun declarations, fix #1199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-08 09:21:06 +02:00
Murphy Berzish
cadde94017 fix indentation and add support for re.allchar 2017-08-07 23:02:55 -04:00
Murphy Berzish
f4c0e0b28d fix regex bug in theory_str for empty string match. need to fix indents 2017-08-06 17:17:04 -04:00
Nikolaj Bjorner
05c4ea82ce Merge pull request #1146 from levnach/dev 
fix get_model in lar_solver
 2017-08-03 14:01:29 -07:00
Nikolaj Bjorner
2f466b6585 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-03 13:56:04 -07:00
Nikolaj Bjorner
91ee52e549 fix #1195 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 13:53:38 -07:00
Lev Nachmanson
95f86ae2c0 more efficient lar_solver::get_model 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
 2017-08-03 11:03:52 -07:00
Lev Nachmanson
712619a9cf fix a but in adjusting term indices for implied_bounds 2017-08-03 10:09:00 -07:00
Nikolaj Bjorner
ffaaa1ff34 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-03 08:50:17 -07:00
Nikolaj Bjorner
8844112418 update header include generation to use relative paths #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 08:50:04 -07:00
Nikolaj Bjorner
4b3251dec1 update API functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-02 16:56:43 -07:00
Nikolaj Bjorner
ce3fd22f3b use common idioms for factor-equivalence code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 21:07:20 -07:00
Arie Gurfinkel
88a35119b9 moved obj_equiv_class to ast 2017-08-01 19:24:50 -04:00
Nikolaj Bjorner
4d07fa5db3 use ifdef instead of if for _TRACE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:46:38 -07:00
Nikolaj Bjorner
be8add44e9 instrument unit test to use reproducible random number generator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 12:42:08 -07:00
Nikolaj Bjorner
22a2aae486 trying to fix build break on use of iterator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 11:47:55 -07:00
Nikolaj Bjorner
3214644e0d Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-01 10:51:52 -07:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger
49d5131f83 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-01 18:33:59 +01:00
Christoph M. Wintersteiger
81a7f37acc Fixed LP tests 2017-08-01 18:33:47 +01:00
Christoph M. Wintersteiger
13c9a6faf7 Merge pull request #1185 from agurfinkel/spacer-nlg-fix 
Spacer nlg fix
 2017-08-01 17:23:23 +01:00
Christoph M. Wintersteiger
aefed78f1a Fixed ML API build again 2017-08-01 17:02:04 +01:00
Christoph M. Wintersteiger
ce01895ab3 Fixed ML API build. 2017-08-01 16:54:27 +01:00
Christoph M. Wintersteiger
4ff938f2c1 Fixed MPF fp.rem(0,0,0). Relates to #872. 2017-08-01 16:46:10 +01:00
Bernhard Gleiss
4559092a0c refactored variable names and added comments to min_cut-related methods for unsat-core-computation 2017-08-01 11:17:06 -04:00
Bernhard Gleiss
bc3d8580c9 fixed typo in optimized unsat core plugin code 2017-08-01 11:17:06 -04:00
Christoph M. Wintersteiger
79ab8a5a5a Fixed cmake build 2017-08-01 16:16:17 +01:00
Christoph M. Wintersteiger
e315d063c5 renamed LP bound propagator to avoid linker name clashes 2017-08-01 16:07:51 +01:00
Christoph M. Wintersteiger
6bc5209e26 Fixed build problems with .vcxproj 2017-08-01 15:53:55 +01:00
Nikolaj Bjorner
72c478078e adding cdecl directive to Z3_qe_lite to address build failure for Java bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 23:14:53 -07:00
Nikolaj Bjorner
1820ccd491 z3-qe-lite? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 22:15:57 -07:00
Nikolaj Bjorner
b12882d94a a few more spacer related warning messages 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 21:56:13 -07:00
Arie Gurfinkel
25c6480e6e updated include directives 2017-07-31 23:16:42 -04:00
Arie Gurfinkel
ecd85b314c more includes 2017-07-31 22:51:28 -04:00
Arie Gurfinkel
66108085fa removing pragmas to make travis happy 2017-07-31 22:51:28 -04:00
Nikolaj Bjorner
c506f3ddc9 fix build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 18:39:35 -07:00
Nikolaj Bjorner
0eb2915e83 Merge pull request #1182 from agurfinkel/spacer-z3 
Spacer
 2017-07-31 17:10:09 -07:00
Nikolaj Bjorner
49cf899207 remove local change 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 16:33:48 -07:00
Nikolaj Bjorner
5cda9504f1 remove relative include from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 16:32:26 -07:00
Christoph M. Wintersteiger
e8cdc34219 Debug fix in fpa2bv converter. Relates to #872. 2017-07-31 22:34:58 +01:00
Arie Gurfinkel
ffff16632d updating includes 2017-07-31 17:30:11 -04:00
Arie Gurfinkel
f465a2225a fixing include paths 2017-07-31 17:14:43 -04:00
Christoph M. Wintersteiger
6a2fa91818 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 22:12:37 +01:00
Christoph M. Wintersteiger
9601761a6f Added missing float conversion in fpa2bv converter. Relates to #1178. 2017-07-31 22:12:15 +01:00
Arie Gurfinkel
97c5ab30d5 small improvements to bmc engine 
courtesy of Marc Brockschmidt
 2017-07-31 17:04:36 -04:00
Arie Gurfinkel
7168451201 eager quantifier instantiation for quantified array properties 2017-07-31 17:04:16 -04:00
Arie Gurfinkel
2c7a39d580 Optionally blast arrays 
This changes the default behavior of always blasting arrays.
The old behavior can be restored using

   fixedpoint.xform.array_blast=true
 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
f5fa6b0bcb optionally disable subsumption checker 2017-07-31 17:03:18 -04:00
Arie Gurfinkel
33c81524d2 optionally disable propagate variable equivalences in interp_tail_simplifier 2017-07-31 17:03:18 -04:00