mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity
6740 commits 23 branches 48 tags 156 MiB
Commit graph

6740 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish 21c8f4aae0 formatting theory_str.cpp 2017-05-05 19:26:15 -04:00
Nikolaj Bjorner 8eb26e25c2 add new files to cmakelist.txt files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-05 17:03:03 -04:00
Nikolaj Bjorner a9fbad53a0 Merge pull request #907 from mtrberzi/release-1.0 
theory_str for Z3 based on the Z3str2 framework
 2017-05-05 16:55:43 -04:00
Murphy Berzish 7ddd43e16d first-class re.range support in theory_str 2017-05-05 15:29:58 -04:00
Murphy Berzish 75ba4d5a4d remove unneeded include 2017-05-05 14:54:36 -04:00
Murphy Berzish 8029b6b889 Merge branch 'upstream-master' into develop 2017-05-05 14:44:29 -04:00
Nikolaj Bjorner 7cb0237ab2 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-05 10:59:58 -04:00
Nikolaj Bjorner 7e1fae418a fix #1005, disable expansion of regular expression range to union as it degrades performance significantly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-05 10:59:47 -04:00
Christoph M. Wintersteiger 79dcf03a42 Enabled C++11 in GCC and Clang 2017-05-05 15:01:10 +01:00
Christoph M. Wintersteiger 00ce3f8172 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-05 14:22:49 +01:00
Christoph M. Wintersteiger 0ebce66c57 Fixed bug with .NET keyfile path containing spaces. Fixes #1003. 2017-05-05 14:22:40 +01:00
Nikolaj Bjorner 9499fa62ac Merge pull request #1004 from delcypher/cmake_doxygen_fixes 
[CMake] Doxygen fixes
 2017-05-04 12:08:10 -07:00
Dan Liew 1db07f1189 [CMake] Remove BYPRODUCTS declaration for api_docs target. 
This breaks the `clean` rule when using Ninja as the CMake
generator. Unfortunately this means `clean` doesn't try to
remove the generated documentation anymore when using Ninja.
 2017-05-04 15:29:47 +01:00
Dan Liew 6261a5c27b Fix bug in mk_api_doc.py where the Z3 python package path would be 
checked when building the Z3 python package documentation was disabled.
 2017-05-04 15:28:20 +01:00
Murphy Berzish c569925676 Merge branch 'upstream-master' into develop 2017-05-03 20:12:11 -04:00
Nikolaj Bjorner a9d6ef68f0 Merge pull request #1002 from mtrberzi/obj_pair_set 
add iterator accessors to obj_pair_set
 2017-05-03 16:18:05 -07:00
Murphy Berzish c2b5e8cfda fix overlap detection internalization 2017-05-03 17:46:06 -04:00
Murphy Berzish ab4fbe40b6 cleanup 2017-05-03 17:45:56 -04:00
Murphy Berzish 41a242fab1 Merge branch 'upstream-master' into develop 
Conflicts:
	src/smt/params/smt_params.h
	src/smt/params/smt_params_helper.pyg
	src/smt/smt_case_split_queue.cpp
	src/smt/smt_context.h
	src/smt/smt_setup.cpp
	src/smt/smt_setup.h
 2017-05-03 17:03:13 -04:00
Murphy Berzish ede6d7bb2b add iterator accessors to obj_pair_set 2017-05-03 14:55:22 -04:00
Nikolaj Bjorner 1177be6391 add common utility to set up seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 20:52:39 -07:00
Nikolaj Bjorner 52dfdedb9b Merge pull request #1000 from mtrberzi/theory_str-smt-setup 
smt_setup for strings/sequences
 2017-05-02 20:44:23 -07:00
Nikolaj Bjorner cc7a176c89 update to retain original behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 19:32:03 -07:00
Nikolaj Bjorner eeb79e1c3c update to retain original behavior 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 19:30:54 -07:00
Nikolaj Bjorner 561a4331a8 add back use of all variables for tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 16:36:05 -07:00
Nikolaj Bjorner cec6ced457 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-02 15:57:41 -07:00
Nikolaj Bjorner 21cda27f5e fix quadratic behavior of extract_assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 15:57:31 -07:00
Nikolaj Bjorner 5b0286001b Merge pull request #999 from mtrberzi/theory-aware-branching 
Theory-aware branching heuristic
 2017-05-02 15:32:37 -07:00
Murphy Berzish 92755b0185 smt_setup framework, all hooks to theory_str are redirected to theory_seq 2017-05-02 17:16:35 -04:00
Nikolaj Bjorner ed0b2be618 fix bug in tracking levels of variables: levels are not cleared, only truth assignment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-02 14:10:07 -07:00
Murphy Berzish a418f0c30b fix spacing 2017-05-02 15:52:35 -04:00
Murphy Berzish e6d527c5d5 remove trace code from theory_arith 2017-05-02 15:39:15 -04:00
Murphy Berzish 15cb2d7dba cleanup 2017-05-02 14:08:48 -04:00
Murphy Berzish a8d069ba46 refactor: add asserts, use case split strategy param 2017-05-02 13:06:08 -04:00
Murphy Berzish 5b4792955d theory-aware branching heuristic 2017-05-02 10:43:40 -04:00
Murphy Berzish 6cd1f877b8 params for theory aware branching 2017-05-02 10:39:32 -04:00
Murphy Berzish 0862949e66 Merge branch 'upstream-master' into develop 
Conflicts:
	src/smt/params/smt_params.cpp
	src/smt/params/smt_params.h
	src/smt/smt_context.cpp
	src/smt/smt_context.h
 2017-05-01 21:33:23 -04:00
Nikolaj Bjorner 48e37b0e16 pass qhead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 16:54:22 -07:00
Nikolaj Bjorner 8ba78081ec fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 16:41:17 -07:00
Nikolaj Bjorner 61e0fc9099 Merge pull request #995 from mtrberzi/theory-case-split 
Theory case split heuristic (for theory_str)
 2017-05-01 15:27:45 -07:00
Murphy Berzish 16a5e944d7 use reference for case split sets 2017-05-01 18:25:54 -04:00
Nikolaj Bjorner f9105edb14 revert to native chunker 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:52 -07:00
Murphy Berzish b86d472eaf simplify theory case split handling 2017-05-01 18:22:49 -04:00
Nikolaj Bjorner d14f2af5ae deal with subtraction that manages to sneak in. Issue #996 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:06 -07:00
Murphy Berzish 3bce61e0d4 fix warning 2017-05-01 10:43:33 -04:00
Murphy Berzish 2f56d128b0 add theory case split support to smt_context 2017-05-01 10:34:43 -04:00
Murphy Berzish f655e1976e add params for theory case split 2017-05-01 10:18:38 -04:00
Nikolaj Bjorner aceee3fac8 renmae to opt_stream_buffer to avoid clash with dimacs stream buffer. #994 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 12:54:29 -07:00
Nikolaj Bjorner 0693a413b6 augment #955 to handle hyphen 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 12:50:56 -07:00
Nikolaj Bjorner 86f3526110 update get-value to also respect parameter model_index, #955 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 11:48:06 -07:00