mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
7724 commits 49 branches 53 tags 182 MiB
Commit graph

7724 commits

This branch
This branch
All branches
Author SHA1 Message Date
Dan Liew
c629dcc53f [Doxygen] Rewrite documentation of Z3_mk_solver() and 
`Z3_mk_simple_solver()` to try to make it clearer what the differences
are between these APIs.

This an attempt to address issues noted in #1035.
 2017-06-11 14:04:18 +01:00
Nikolaj Bjorner
f44a3e1bbc print_core as a function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 10:18:07 -07:00
Nikolaj Bjorner
8acb37e734 revert change to 1065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:45:18 -07:00
Nikolaj Bjorner
582a069c51 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-10 09:31:02 -07:00
Nikolaj Bjorner
b8e8e090ad filter assumptions by membership in initial list #1065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:30:01 -07:00
Nikolaj Bjorner
d5f646929e print success #1068 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:16:36 -07:00
Nikolaj Bjorner
ed0e06c7ac Merge pull request #1066 from delcypher/misc_doxygen_fixes 
Misc doxygen fixes
 2017-06-08 09:21:06 -07:00
Dan Liew
bcb3981c5f [Doxygen] Fixed mismatched @{ and @} declaration which prevented 
the `capi` group from being declared properly. For example this
prevented from `Z3_mk_solver()` from appearing in the `capi` group.
 2017-06-07 18:49:43 +01:00
Dan Liew
85c7f5d865 [Doxygen] Fix some Doxygen warnings for z3_optimization.h 2017-06-07 18:45:12 +01:00
Dan Liew
903709b9c1 [Doxygen] Fix bug where some header files were not being scanned. 2017-06-07 17:09:01 +01:00
Christoph M. Wintersteiger
0137104683 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-06 16:04:45 +01:00
Christoph M. Wintersteiger
83e9c40265 Added __deepcopy__ operators to ref-counted objects in the Python API 2017-06-06 16:04:38 +01:00
Nikolaj Bjorner
af285d02c3 add documentation per #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-05 08:38:28 -07:00
Nikolaj Bjorner
4f04301305 add documentation per #1058 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-05 07:55:32 -07:00
Nikolaj Bjorner
a8ff97c0f4 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-04 11:05:21 -07:00
Nikolaj Bjorner
668bad6121 print success after reset assertions #1057 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-04 11:04:54 -07:00
Nikolaj Bjorner
efd5727676 add shorthand for enumerating constants in a model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-02 10:35:09 -07:00
Nikolaj Bjorner
2908ab4069 fix reference count issue with pinning to expr_ref 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:56:25 -07:00
Nikolaj Bjorner
e9ed3af455 fix regression in str 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:35:35 -07:00
Nikolaj Bjorner
fda59f5a24 expose operator kinds for internal functions using their sequence variants. Issue #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:32:17 -07:00
Nikolaj Bjorner
1fa60f4893 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-01 09:11:09 -07:00
Nikolaj Bjorner
52e0f3b539 add string accessors to managed APIs #1051 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-01 09:10:49 -07:00
Christoph M. Wintersteiger
596652ed36 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-31 18:35:52 +01:00
Christoph M. Wintersteiger
4f0a87299c Fixed signed/unsigned comparison warnings 2017-05-31 18:35:06 +01:00
Christoph M. Wintersteiger
a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner
546d22e77a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-30 11:18:43 -07:00
Nikolaj Bjorner
415824b600 put temporaries on trail 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-30 11:18:33 -07:00
Nikolaj Bjorner
2cfb9eec3d Merge pull request #1050 from pathawks/fix-markdown 
Fix Markdown heading
 2017-05-30 11:03:07 -07:00
Pat Hawks
e6d3b732e9 Remove tab 2017-05-30 12:53:55 -05:00
Nikolaj Bjorner
870017e2ce Merge pull request #1049 from chaserhkj/java-api-update-fix 
`Expr.update()` in java API should not return super class
 2017-05-29 18:14:54 -07:00
KangJing Huang (Chaserhkj)
8092dd5aa3 Fix Expr.update in java API returning superclass 2017-05-29 20:51:42 -04:00
Nikolaj Bjorner
4cbf938cf3 enable get-unsat-assumptions command per request in #1048 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 16:26:22 -07:00
Nikolaj Bjorner
2de80b5ce9 add pb built in ops for logic ALL #1045 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 10:08:50 -07:00
Nikolaj Bjorner
d95ac58bad remove throw in reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 12:09:35 -07:00
Nikolaj Bjorner
f80a622a8f add colon to assertion stack levels #1046 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-28 11:10:46 -07:00
Nikolaj Bjorner
1654ad7059 adding escape characters to reason-unknown #1043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-27 14:56:38 -07:00
Nikolaj Bjorner
f3a0b7e0cd change command-line experience for pareto fronts. It now requires multiple check-sat calls to loop over the fronts. This allows querying each model in turn. #1008 2017-05-23 20:05:10 -07:00
Nikolaj Bjorner
49faaaa8f1 allowing non-literal assumptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 15:01:00 -07:00
Nikolaj Bjorner
6f2cd4817b ensure arith.reflect has default true 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 14:09:45 -07:00
Nikolaj Bjorner
3f89c1418b fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 12:51:14 -07:00
Nikolaj Bjorner
23ff580a67 get rid of timeb dependencies, pull request #1040 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 12:16:43 -07:00
Nikolaj Bjorner
edb164587f get rid of a simplifier dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 10:12:32 -07:00
Nikolaj Bjorner
af4346f16a expose arith reflection, get rid of long m_manager attribute in asserted fromulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 10:04:29 -07:00
Nikolaj Bjorner
2834fea9b3 fix x64 warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 08:58:21 -07:00
Nikolaj Bjorner
90af406338 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-23 08:51:38 -07:00
Nikolaj Bjorner
8e9739d3b0 work around crash #1039 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 08:51:26 -07:00
Nikolaj Bjorner
2cbeedec69 accept hereditarily finite sorts in datalog engine 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-22 19:32:43 -07:00
Nikolaj Bjorner
622d8c951c remove redundant data-type function declarations from pretty-printed output. #1034 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-22 14:40:42 -07:00
Nikolaj Bjorner
cfd598fabb Merge pull request #1036 from delcypher/cmake_remove_foci2_stub 
[CMake] Remove FOCI2 stub code.
 2017-05-22 09:20:54 -07:00
Nikolaj Bjorner
2a26c2c65f Merge pull request #1037 from delcypher/cmake_log_sync 
[CMake] Add CMake option `API_LOG_SYNC` that corresponds to the
 2017-05-22 09:20:33 -07:00