mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity
6823 commits 23 branches 48 tags 156 MiB
Commit graph

6823 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner d6e2e1f28f Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 11:28:26 -07:00
Nikolaj Bjorner aff02ca905 include 'stopwatch.h' to avoid ODR warnings, #994 2017-04-30 11:28:11 -07:00
Nikolaj Bjorner bd1b930d7a swap argument order of chunk with file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 11:00:03 -07:00
Nikolaj Bjorner 5fcbf55216 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-30 10:23:05 -07:00
Nikolaj Bjorner 2c208e1d10 Sat update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-30 10:23:00 -07:00
Nikolaj Bjorner 4468816d32 fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 19:00:15 -07:00
Nikolaj Bjorner b3f720c2bf fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 18:58:34 -07:00
Nikolaj Bjorner 3152833893 fix unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 18:55:47 -07:00
Nikolaj Bjorner 944dfbc6ef Merge branch 'master' of https://github.com/Z3Prover/z3 2017-04-29 17:39:20 -07:00
Nikolaj Bjorner fa868e058e fix bound bug #991 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-04-29 17:39:02 -07:00
Nikolaj Bjorner d3f9e4874a Merge pull request #993 from delcypher/cmake_fix_setting_flags 
[CMake] Make MSVC flags much more similar to python/Makefile build system.
 2017-04-29 11:35:37 -07:00
Dan Liew 6e07d6dd2d [CMake] Override CMake's default flags for GCC/Clang as we were doing 
before 4cc2b292c0.

It's useful to be able to control the defaults and CMake's internal
logic for GCC/Clang is simple enough that doing this makes sense.

It would be nice to do the same for MSVC but CMake's internal
logic is more complicated so for now it's better that we just use
CMake's default.
 2017-04-29 17:45:02 +01:00
Dan Liew 2a919cf16e [CMake] Duplicate the remaining linker flags from the old build system. 2017-04-29 16:22:46 +01:00
Dan Liew d032dbcbb2 [CMake] When using MSVC set the /SUBSYSTEM: argument given to 
the linker. This mimics the behaviour of the old build system.
 2017-04-29 16:22:46 +01:00
Dan Liew 364bcde6c1 [CMake] When building with MSVC pass the /STACK: argument to the 
linker like the old build system does.
 2017-04-29 16:22:46 +01:00
Dan Liew c9aac0ba77 [CMake] When building with MSVC try to disable incremental linking 
for all builds.
 2017-04-29 16:22:46 +01:00
Dan Liew 5893aea602 [CMake] When building with MSVC and without WARNINGS_AS_ERRORS 
pass `/WX-` to MSVC. Although this is not necessary this duplicates
the behaviour of the old build system.
 2017-04-29 16:22:46 +01:00