3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
z3/src/test
Nikolaj Bjorner 4d3d9f7602 include compression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-11 20:32:39 -07:00
..
fuzzing Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 2012-12-18 17:14:25 -08:00
algebraic.cpp Fix typos and bugs. Add tests. 2013-01-04 15:01:27 -08:00
api.cpp type check distinct operator. fixes #62 2015-04-27 11:10:37 -07:00
api_bug.cpp checkpoint 2012-10-23 12:12:59 -07:00
arith_rewriter.cpp add normalizer of monomial coefficients 2013-08-10 10:50:03 -07:00
arith_simplifier_plugin.cpp removed front-end-params 2012-12-02 10:05:29 -08:00
ast.cpp add hilbert basis utility for extracting auxiliary invariants 2013-02-12 14:58:04 -08:00
bit_blaster.cpp checkpoint 2012-10-21 22:16:58 -07:00
bit_vector.cpp add unit test for previous commit 2013-03-22 11:51:28 -07:00
bits.cpp checkpoint 2012-10-21 22:16:58 -07:00
buffer.cpp checkpoint 2012-10-21 22:16:58 -07:00
bv_simplifier_plugin.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
chashtable.cpp checkpoint 2012-10-21 22:16:58 -07:00
check_assumptions.cpp removed front-end-params 2012-12-02 10:05:29 -08:00
datalog_parser.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
ddnf.cpp include compression 2015-05-11 20:32:39 -07:00
diff_logic.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
dl_context.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_product_relation.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_query.cpp merge unstable into opt 2014-09-26 12:12:24 -07:00
dl_relation.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_table.cpp re-organize muz_qe into separate units 2013-08-28 21:20:24 -07:00
dl_util.cpp checkpoint 2012-10-21 22:16:58 -07:00
doc.cpp fixing udoc/adding tuned join_project 2014-10-08 22:07:19 -07:00
escaped.cpp checkpoint 2012-10-21 22:16:58 -07:00
ex.cpp checkpoint 2012-10-21 22:16:58 -07:00
expr_rand.cpp Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 2012-12-18 17:14:25 -08:00
expr_substitution.cpp test case for non-termination of substitution/rewriting 2013-09-24 05:33:16 +03:00
ext_numeral.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
f2n.cpp checkpoint 2012-10-21 22:16:58 -07:00
factor_rewriter.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
fixed_bit_vector.cpp fix overflow bugs in doc 2014-09-22 22:03:59 -07:00
for_each_file.cpp checkpoint 2012-10-21 22:16:58 -07:00
for_each_file.h checkpoint 2012-10-21 22:16:58 -07:00
get_implied_equalities.cpp fix get_implied equalities and the unit test 2012-12-11 21:39:31 -08:00
hashtable.cpp checkpoint 2012-10-21 22:16:58 -07:00
heap.cpp checkpoint 2012-10-21 22:16:58 -07:00
heap_trie.cpp test hilbert-basis with fdds and checked integers 2013-03-26 17:31:11 -07:00
hilbert_basis.cpp fix sorting network bug, add network compilation,... 2014-09-11 18:47:21 -07:00
horn_subsume_model_converter.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
hwf.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:16:26 -07:00
im_float_config.h checkpoint 2012-10-21 22:16:58 -07:00
inf_rational.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
interval.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
karr.cpp fix compiler warnings and errors 2013-04-03 17:03:07 -07:00
list.cpp checkpoint 2012-10-21 22:16:58 -07:00
main.cpp add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core 2015-05-09 19:40:34 -07:00
map.cpp fixing some compilation warnings 2012-10-24 23:43:58 -07:00
matcher.cpp fix a few compilation warnings 2013-04-21 14:36:39 -07:00
memory.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
model2expr.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
model_retrieval.cpp Make ast_manager::get_family_id(symbol const &) side-effect free. The version with side-effects is now called ast_manager::mk_family_id 2012-12-18 17:14:25 -08:00
mpbq.cpp checkpoint 2012-10-21 22:16:58 -07:00
mpf.cpp checkpoint 2012-10-21 22:16:58 -07:00
mpff.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
mpfx.cpp checkpoint 2012-10-21 22:16:58 -07:00
mpq.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
mpz.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
nlarith_util.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
nlsat.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
no_overflow.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
object_allocator.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
old_interval.cpp checkpoint 2012-10-21 22:16:58 -07:00
optional.cpp checkpoint 2012-10-21 22:16:58 -07:00
parray.cpp Fixed warnings produced by gcc 4.6.3 when compiling in debug mode 2012-10-30 23:43:00 -07:00
pdr.cpp Codeplex issue 191: inconsistent results from PDR engine. The report exposed bugs in the implementation of the priority queue leaving unexplored leaves durin search. The priority queue has now been revised to address the exposed bugs 2015-04-01 16:27:15 -07:00
permutation.cpp fixed more compilation errors reported by g++ 4.7.1 2012-10-27 22:32:50 -07:00
polynomial.cpp Added support for clang++ on OSX 2012-11-12 04:56:48 +00:00
polynomial_factorization.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
polynorm.cpp more on polynorm 2013-08-14 11:55:23 -07:00
prime_generator.cpp checkpoint 2012-10-21 22:16:58 -07:00
proof_checker.cpp checkpoint 2012-10-21 22:16:58 -07:00
qe_arith.cpp Fix build of test 2013-09-15 04:24:20 -07:00
quant_elim.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
quant_solve.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
random.cpp checkpoint 2012-10-21 22:16:58 -07:00
rational.cpp Fix is_int64 bug in mpz when compiling with GMP 2013-04-08 14:50:17 -07:00
rcf.cpp Fix memory allocation problems in RCF module 2013-04-10 19:03:25 -07:00
region.cpp checkpoint 2012-10-21 22:16:58 -07:00
sat_user_scope.cpp implement user scopes for sat solver 2014-07-30 09:27:03 -07:00
simple_parser.cpp Isolating reg_decl_plugins 2012-10-24 11:27:50 -07:00
simplex.cpp fix wrong simplex backtracking 2014-05-09 08:51:07 -07:00
simplifier.cpp compiler optimization and fixes to unit tests 2013-04-11 13:44:23 -07:00
small_object_allocator.cpp checkpoint 2012-10-21 22:16:58 -07:00
smt2print_parse.cpp checkpoint 2012-10-21 22:16:58 -07:00
smt_context.cpp removed front-end-params 2012-12-02 10:05:29 -08:00
sorting_network.cpp adding unit tests for doc 2014-09-18 05:19:52 -07:00
stack.cpp checkpoint 2012-10-21 22:16:58 -07:00
string_buffer.cpp checkpoint 2012-10-21 22:16:58 -07:00
substitution.cpp update substitution routines 2013-01-21 21:59:20 -08:00
symbol.cpp checkpoint 2012-10-21 22:16:58 -07:00
symbol_table.cpp checkpoint 2012-10-21 22:16:58 -07:00
tbv.cpp fixing udoc/adding tuned join_project 2014-10-08 22:07:19 -07:00
test_util.h checkpoint 2012-10-21 22:16:58 -07:00
theory_dl.cpp removed front-end-params 2012-12-02 10:05:29 -08:00
theory_pb.cpp fix wrong simplex backtracking 2014-05-09 08:51:07 -07:00
timeout.cpp checkpoint 2012-10-23 12:12:59 -07:00
total_order.cpp checkpoint 2012-10-21 22:16:58 -07:00
trigo.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
udoc_relation.cpp muZ/datalog/udoc: fix bug in join_project 2014-12-28 17:05:17 +00:00
uint_set.cpp checkpoint 2012-10-21 22:16:58 -07:00
upolynomial.cpp Fixed warnings reported by gcc 4.7.1 2012-10-31 00:05:38 -07:00
var_subst.cpp updating tests 2013-02-12 18:13:02 -08:00
vector.cpp Adding overflow checks 2013-09-02 19:43:22 -07:00