Nikolaj Bjorner 2f756da294 adding dt-solver (#4739) ... * adding dt-solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * dt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * move mbp to self-contained module Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * files Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Create CMakeLists.txt * dt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * rename to bool_var2expr to indicate type class * mbp * na		2020-10-18 15:28:21 -07:00
..
fuzzing	booyah	2020-07-04 15:56:30 -07:00
lp	Lpbounds (#4492)	2020-06-02 01:00:06 -07:00
algebraic.cpp	print roots as part of test	2020-03-24 15:28:51 -07:00
api.cpp
api_bug.cpp
arith_rewriter.cpp	build	2018-10-06 15:16:23 -07:00
arith_simplifier_plugin.cpp
ast.cpp	Fix some spelling errors (mostly in comments).	2018-10-20 17:07:41 +02:00
bdd.cpp	fixes to reset	2019-12-28 15:31:20 -08:00
bit_blaster.cpp	remove dependency on ARRAYSIZE for issue #1616	2018-08-15 22:26:14 -07:00
bit_vector.cpp	bool_vector, some spacer tidy	2020-04-05 12:59:04 -07:00
bits.cpp
buffer.cpp
chashtable.cpp	Prefer using empty rather than size comparisons.	2018-11-27 21:42:04 +07:00
check_assumptions.cpp
CMakeLists.txt	euf	2020-08-24 01:55:13 -07:00
cnf_backbones.cpp	fix test	2019-02-06 20:13:21 +01:00
cube_clause.cpp
datalog_parser.cpp
ddnf.cpp	Fix some spelling errors (mostly in comments).	2018-10-20 17:07:41 +02:00
diff_logic.cpp	fix unit test build	2020-04-30 14:49:49 -07:00
dl_context.cpp	prepare symbols to be more abstract, update mbi, delay initialize some modules	2020-01-10 12:02:08 -08:00
dl_product_relation.cpp	prepare symbols to be more abstract, update mbi, delay initialize some modules	2020-01-10 12:02:08 -08:00
dl_query.cpp
dl_relation.cpp	prepare symbols to be more abstract, update mbi, delay initialize some modules	2020-01-10 12:02:08 -08:00
dl_table.cpp	prepare symbols to be more abstract, update mbi, delay initialize some modules	2020-01-10 12:02:08 -08:00
dl_util.cpp
doc.cpp	bool_vector, some spacer tidy	2020-04-05 12:59:04 -07:00
egraph.cpp	bv and gc of literals (#4692)	2020-09-17 14:24:07 -07:00
escaped.cpp
ex.cpp
expr_rand.cpp	fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string	2020-07-11 20:24:45 +01:00
expr_substitution.cpp
ext_numeral.cpp
f2n.cpp
factor_rewriter.cpp
finder.cpp	Testcase for npn3_finder.	2020-03-01 04:10:25 -08:00
fixed_bit_vector.cpp
for_each_file.cpp	remove dependency on ARRAYSIZE for issue #1616	2018-08-15 22:26:14 -07:00
for_each_file.h	booyah	2020-07-04 15:56:30 -07:00
get_consequences.cpp	fix include paths	2018-08-05 13:49:26 -07:00
get_implied_equalities.cpp
hashtable.cpp
heap.cpp	reduce output	2018-12-17 17:05:48 -08:00
heap_trie.cpp
hilbert_basis.cpp	fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string	2020-07-11 20:24:45 +01:00
horn_subsume_model_converter.cpp
hwf.cpp
im_float_config.h	booyah	2020-07-04 15:56:30 -07:00
inf_rational.cpp
interval.cpp	fix the test build	2020-01-28 10:04:21 -08:00
karr.cpp
list.cpp
main.cpp	euf	2020-08-24 01:55:13 -07:00
map.cpp
matcher.cpp	#2117	2019-01-30 09:34:45 -08:00
memory.cpp
model2expr.cpp
model_based_opt.cpp
model_evaluator.cpp
model_retrieval.cpp
mpbq.cpp
mpf.cpp
mpff.cpp	Fixing build errors when building test-z3 (#4496)	2020-06-03 13:34:43 -07:00
mpfx.cpp
mpq.cpp
mpz.cpp	address min-int overflow reported in #2565	2019-09-17 18:19:55 -04:00
nlarith_util.cpp
nlsat.cpp	na	2019-11-03 10:29:10 +01:00
no_overflow.cpp	Switch from using Z3_bool to using bool.	2018-11-20 11:27:09 +07:00
object_allocator.cpp
old_interval.cpp	janitor services	2020-06-03 10:15:55 -07:00
optional.cpp
parray.cpp
pb2bv.cpp	fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string	2020-07-11 20:24:45 +01:00
pdd.cpp	Nikolaj fixes pdd_manager::reduce() to work with the changed order	2020-01-28 10:04:21 -08:00
pdd_solver.cpp	fix unit test	2020-01-05 17:52:44 -08:00
permutation.cpp
polynomial.cpp
polynorm.cpp	build	2018-10-06 15:16:23 -07:00
prime_generator.cpp	fix crash in 'test-z3 prime_generator'	2019-06-13 14:35:52 +01:00
proof_checker.cpp
qe_arith.cpp	adding dt-solver (#4739)	2020-10-18 15:28:21 -07:00
quant_elim.cpp
quant_solve.cpp	build	2018-10-06 15:16:23 -07:00
random.cpp
rational.cpp
rcf.cpp
region.cpp
sat_local_search.cpp	include chronological backtracking, two-phase sat, xor inprocessing, probsat, ddfw	2019-06-13 08:45:21 -07:00
sat_lookahead.cpp	fix test build	2018-11-14 12:04:31 -08:00
sat_user_scope.cpp
simple_parser.cpp
simplex.cpp	avoid going creating hnf_cuts if all involved vars have integral values	2018-06-27 12:16:58 -07:00
simplifier.cpp
small_object_allocator.cpp
smt2print_parse.cpp	Use nullptr.	2018-10-02 09:11:19 +07:00
smt_context.cpp
solver_pool.cpp
sorting_network.cpp	add binary_merge encoding option	2019-02-28 08:35:22 -08:00
stack.cpp
string_buffer.cpp
substitution.cpp
symbol.cpp
symbol_table.cpp
tbv.cpp	arrays (#4684)	2020-09-13 19:29:59 -07:00
test_util.h
theory_dl.cpp	prepare symbols to be more abstract, update mbi, delay initialize some modules	2020-01-10 12:02:08 -08:00
theory_pb.cpp	fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string	2020-07-11 20:24:45 +01:00
timeout.cpp
total_order.cpp
trigo.cpp
udoc_relation.cpp
uint_set.cpp	bool_vector, some spacer tidy	2020-04-05 12:59:04 -07:00
upolynomial.cpp	bool_vector, some spacer tidy	2020-04-05 12:59:04 -07:00
value_generator.cpp	na	2020-04-25 13:13:25 -07:00
value_sweep.cpp	value sweep	2020-04-27 18:58:43 -07:00
var_subst.cpp	integrate lambda expressions	2018-06-26 07:23:04 -07:00
vector.cpp	Prefer using empty rather than size comparisons.	2018-11-27 21:42:04 +07:00