mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
8888 commits 23 branches 48 tags 157 MiB
Commit graph

8888 commits

This branch
This branch
All branches
Author SHA1 Message Date
Miguel Angelo Da Terra Neves
1e22cb73d5 merge 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-11 14:14:44 -08:00
Miguel Angelo Da Terra Neves
9f0a8af255 fixed adaptive apsat 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-11 14:14:16 -08:00
Nikolaj Bjorner
35a3523fd6 fix bug in double collection of declarations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-11 14:09:34 -08:00
Nikolaj Bjorner
82c26509ae
Merge pull request #1396 from mtrberzi/substr-bug 
Fix incorrect term in theory_str str.substr reduction
 2017-12-11 12:36:07 -08:00
Nikolaj Bjorner
6d729f1f15 disable UHLT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-11 10:36:42 -08:00
Murphy Berzish
83bd103cd4 Merge remote-tracking branch 'upstream/master' into develop 2017-12-11 13:05:04 -05:00
Christoph M. Wintersteiger
2e186633ee Turned assertion failure into proper error message. 2017-12-11 14:59:25 +00:00
Murphy Berzish
9d2c86f214 fix incorrect clause in argumentsValid subterm of substr reduction 2017-12-08 20:31:22 -05:00
Nikolaj Bjorner
faebbc5384 add shortcuts for concatenation and equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 16:17:04 +05:30
Nikolaj Bjorner
c8d9be0bbf fix build of obj_ref_hashtable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 14:22:25 +05:30
Nikolaj Bjorner
a5d5dfdf86 fix setup for non-linear real arithmetic per QF_UFNRA regresssions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 09:23:57 +05:30
Nikolaj Bjorner
3f19c12a12 add obj_ref_map to make it easier to maintain reference counts with a map of objects 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 05:48:34 +05:30
Nikolaj Bjorner
8c8d229ca9 Merge branch 'master' of https://github.com/z3prover/z3 2017-12-07 18:43:53 +05:30
Nikolaj Bjorner
8e1ab23c3d remove deprecated functions from ML API. #1393 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-07 18:43:29 +05:30
Nikolaj Bjorner
0cfea8946b
Merge pull request #1391 from delcypher/cxx_example_use_cxx11 
[CMake] Use C++11 is C++ API example
 2017-12-07 18:38:05 +05:30
Dan Liew
1941a53999 [Release Notes] Note that C++11 is required to build Z3 and is also 
required by the C++ API bindings.
 2017-12-07 10:56:44 +00:00
Dan Liew
92059942e6 [CMake] Use C++11 when building C++ API example. 
This is a change requested by @NikolajBjorner (
5f8c97532c (commitcomment-26049417)
).
 2017-12-07 10:56:44 +00:00
Murphy Berzish
9554723b44 use safer mk_and in extended indexof 2017-12-06 20:50:03 -05:00
Nikolaj Bjorner
39d1ad3edb fix #1390 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-07 05:15:53 +05:30
Murphy Berzish
a5c828f6f2 length estimation 2017-12-06 18:32:11 -05:00
Nikolaj Bjorner
9ff724ec6d
Merge pull request #11 from TheRealNebus/opt 
Opt
 2017-12-05 18:03:24 -08:00
Miguel Angelo Da Terra Neves
38751430df adaptive psat cutoff 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-05 17:53:48 -08:00
Nikolaj Bjorner
2770c8f884 disable C++11 dependency to fix the travis build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-05 08:15:23 +05:30
Murphy Berzish
fbe8d1577e new regex automata start; add complexity estimation 2017-12-04 18:05:00 -05:00
Miguel Angelo Da Terra Neves
d8a62dff73 merge 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-04 14:34:59 -08:00
Miguel Angelo Da Terra Neves
e0dfbd6d1c fixed freevars and psat cube cutoffs 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-04 14:33:48 -08:00
Nikolaj Bjorner
60af4a5820 deal with ambiguity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-04 19:12:51 +05:30
Nikolaj Bjorner
5f8c97532c circumvent build errors introduced when using the ast_vector_tpl iterator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-04 18:10:48 +05:30
Nikolaj Bjorner
fb470a1868 include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-04 15:32:20 +05:30
Nikolaj Bjorner
a83af22841 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:45 +01:00
Nikolaj Bjorner
5ee30a3cd9 include special functionality in parsers for solvers and opt for additional file formats 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-03 20:00:24 +01:00
Nikolaj Bjorner
187998ae4d
Merge pull request #1381 from NikolajBjorner/smt2 
remove smtlib1 dependencies
 2017-12-02 10:24:02 -08:00
Nikolaj Bjorner
fc3cbcbe02 remove deprecated options 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-02 10:16:35 -08:00
Nikolaj Bjorner
b98c864d76 fixes to inprocessing code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 18:06:26 -08:00
Nikolaj Bjorner
0bfea99cff fix issues found in parsing examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 14:43:52 -08:00
Miguel Angelo Da Terra Neves
2e042a8bea Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-12-01 11:02:35 -08:00
Miguel Angelo Da Terra Neves
1b7cb110d3 freevars cube cutoff 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-12-01 11:02:29 -08:00
Nikolaj Bjorner
c8e655830f add statistics to cubing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 10:13:54 -08:00
Nikolaj Bjorner
274279b251 Merge branch 'smt2' of https://github.com/nikolajbjorner/z3 into smt2 2017-12-01 09:00:01 -08:00
Nikolaj Bjorner
a9ebda105c remove assertion that gets violated on exception path (declaration of datatypes are not getting removed) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 08:59:36 -08:00
Nikolaj Bjorner
e0d28c67cd Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-12-01 08:25:05 -08:00
Nikolaj Bjorner
a9f32cd382 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-12-01 08:24:51 -08:00
Nikolaj Bjorner
e0d69a0033 fix perf bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 08:24:42 -08:00
Nikolaj Bjorner
018411bc58 fix bug in PB constraint init_watch handling, adding transitive reduction, HLE, ULT, 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 08:23:55 -08:00
Nikolaj Bjorner
8357210d3c fix lack of warning/error for unbounded objectives in context of quantifiers #1382 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 01:07:41 -08:00
Nikolaj Bjorner
c31ad14747 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:32 -08:00
Nikolaj Bjorner
4bb0e9b633 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-01 00:52:06 -08:00
Nikolaj Bjorner
427b5ef002 set eliminated to false on literals used in clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-30 11:20:19 -08:00
Nikolaj Bjorner
b96dacfff2 set version, fix build of test files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-30 08:42:01 -08:00
Nikolaj Bjorner
da0aa71082 adding uhle/uhte for faster asymmetric branching 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-29 21:21:56 -08:00