5989 commits

Author	SHA1	Message	Date
Dan Liew	89c8f1722f	Fix typo that prevented uses of bvsmod_i being parsed.	2017-07-12 12:53:10 +01:00
Lev Nachmanson	2056404ed4	branch on a free variable before trying Gomory cuts ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-11 16:44:04 -07:00
Lev Nachmanson	bac16bac85	start gomory cut ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-11 13:46:46 -07:00
Lev Nachmanson	fc6a876845	start gomory cut ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-11 13:38:59 -07:00
Jack Feser	0e45777104	add get_num_scopes to python solver api	2017-07-11 14:42:34 -04:00
Murphy Berzish	86e7f83e06	proper theory_arith integration in theory_str::get_arith_value()	2017-07-11 13:24:48 -04:00
Lev Nachmanson	69d6b022b8	speed up in get_model and fix in git_model_do_not_care_... ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-10 22:14:56 -07:00
Lev Nachmanson	2fe846d9fc	fix a bug in the lar_solver::m_status update during push/pop ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-10 16:34:23 -07:00
Lev Nachmanson	581098299b	change the order of initializations in the constructor of imp in theory_lra ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-10 12:04:58 -07:00
Lev Nachmanson	9dc7ba73eb	use a faster version of get_model in debug checks ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-10 11:57:33 -07:00
Lev Nachmanson	86ed01a63b	replace clp to clean ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-10 11:30:08 -07:00
Lev Nachmanson	cc32e45471	replace lean to lp ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-10 11:06:37 -07:00
Nikolaj Bjorner	2b0106c199	doc fixes ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-09 11:26:27 +02:00
Nikolaj Bjorner	2af08a378d	avoid complaining about division by 0 as unhandled in theory-lra ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-08 18:21:47 -07:00
Nikolaj Bjorner	5714f830b0	fix check for finite sorts #1122 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-08 13:37:24 -07:00
Lev Nachmanson	f6a75600c2	solve all smt2 from QF_LIA/calypto with int_solver ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-07 22:15:47 -07:00
Nikolaj Bjorner	55f54b4fdc	fixing overflow checking ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-07 13:53:26 -07:00
Lev Nachmanson	3abc793876	solve more integer smt problems	2017-07-07 11:47:52 -07:00
Nikolaj Bjorner	ea331ebfbe	revert update to #1134 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-07 08:29:16 -07:00
Nikolaj Bjorner	d06e48a361	detect overlapping signatures #1134 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-07 08:13:14 -07:00
Nikolaj Bjorner	49cf3f8008	update documentation according to #1058 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-07 07:44:55 -07:00
Nikolaj Bjorner	53c38f02d5	n/a ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-06 22:12:18 -07:00
Lev Nachmanson	2cd81851e7	solve more ilp smt ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-07-06 21:29:09 -07:00
Lev Nachmanson	7cd6dc1b5a	Merge branch 'master' of https://github.com/levnach/z3	2017-07-06 20:47:19 -07:00
Nikolaj Bjorner	055593469a	Dev (#64) ... * introduce int_solver.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add int_solver class Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * track which var is an integer Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add queries for integrality of vars Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * resurrect lp_tst in its own director lp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add_constraint has got a body Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix add_constraint and substitute_terms_in_linear_expression Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * after merge with Z3Prover Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding stub check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#51) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * test Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * Dev (#53) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * preserve is_int flag Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a debug printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#54) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use integer test from lra solver, updated it to work on term variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix equality check in assume-eq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix model_is_int_feasible Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * untested gcd_test() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * call fill_explanation_from_fixed_columns() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * port more of theory_arith_int.h Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * use statistics of lar_solver by theory_lra.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * port more code to int_solver.cpp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add an assert Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * more int porting Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a bug in pivot_fixed_vars_from_basis Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * small change Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * implement find_inf_int_base_column() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * catch unregistered vars in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add a file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * compile for vs2012 Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix asserts in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix the lp_solver init when workig on an mps file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * towards int_solver::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * change in int_solver::check() signature Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * return branch from int_solver::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add a stub for mk_gomory_cut Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * Dev (#59) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#60) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#61) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more TRACE(arith_int) Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix the build Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#62) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build fix Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-06 20:47:07 -07:00
Lev Nachmanson	9b1b096a16	fix in init_int_int_set ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-07-06 20:46:17 -07:00
Lev Nachmanson	0e0e9c7041	correct handling of integer vars by NB ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-06 14:06:33 -07:00
Lev Nachmanson	2e95a9d6b2	return a value from pivot_column_general ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-06 10:59:20 -07:00
Lev Nachmanson	b21741cccd	fix a bug in pivot_fixed_vars_from_basis ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-07-06 10:53:32 -07:00
Nikolaj Bjorner	4c23527974	Dev (#63) ... * introduce int_solver.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add int_solver class Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * track which var is an integer Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add queries for integrality of vars Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * resurrect lp_tst in its own director lp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add_constraint has got a body Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix add_constraint and substitute_terms_in_linear_expression Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * after merge with Z3Prover Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding stub check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#51) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * test Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * Dev (#53) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * preserve is_int flag Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a debug printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#54) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use integer test from lra solver, updated it to work on term variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix equality check in assume-eq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix model_is_int_feasible Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * untested gcd_test() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * call fill_explanation_from_fixed_columns() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * port more of theory_arith_int.h Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * use statistics of lar_solver by theory_lra.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * port more code to int_solver.cpp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add an assert Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * more int porting Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a bug in pivot_fixed_vars_from_basis Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * small change Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * implement find_inf_int_base_column() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * catch unregistered vars in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add a file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * compile for vs2012 Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix asserts in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix the lp_solver init when workig on an mps file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * towards int_solver::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * change in int_solver::check() signature Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * return branch from int_solver::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add a stub for mk_gomory_cut Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * Dev (#59) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#60) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#61) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more TRACE(arith_int) Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix the build Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#62) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build fix Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-06 08:53:08 -07:00
Nikolaj Bjorner	da263601e6	n/a ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-05 19:19:36 -07:00
Nikolaj Bjorner	b419a0e4a4	n/a ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-05 14:32:13 -07:00
Nikolaj Bjorner	465ed7d068	adding doc #1132 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-05 10:21:57 -07:00
Murphy Berzish	b14364a117	fix theory_str warnings: rename get_value() to get_arith_value()	2017-07-05 11:06:40 -04:00
Nikolaj Bjorner	41803ec1cf	fix trace/debug build for unreferenced variables ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 19:55:38 -07:00
Nikolaj Bjorner	cba9a160d3	deal with warning messages ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 19:42:22 -07:00
Nikolaj Bjorner	5b8e3ae198	Merge pull request #1129 from mtrberzi/fix-warnings ... clean up warnings in theory_str	2017-07-04 19:41:43 -07:00
Nikolaj Bjorner	bd92797663	fix compiler warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 15:25:59 -07:00
Nikolaj Bjorner	d66db280a8	fix compiler warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 13:43:32 -07:00
Nikolaj Bjorner	a1306eaab6	fix compiler warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 13:17:37 -07:00
Nikolaj Bjorner	253870c6d7	fix compiler warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 13:08:23 -07:00
Nikolaj Bjorner	5262248823	n/a ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 11:13:05 -07:00
Murphy Berzish	03fe3d74f8	clean up warnings in theory_str	2017-07-04 13:28:18 -04:00
Nikolaj Bjorner	4132c44f8d	update to avoid difference in debug/release builds ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-02 16:24:59 -07:00
Nikolaj Bjorner	480296ed96	updates ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-02 11:27:02 -07:00
Nikolaj Bjorner	031d7e1b59	use iterators, update build icon for osx ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-01 16:58:40 -07:00
Nikolaj Bjorner	08524a2d90	cleanup for warning message ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-01 11:47:17 -07:00
Nikolaj Bjorner	be4b0ffe69	fix unsoundness bug instroduced when fixing #1125 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-06-30 19:36:38 -07:00
Nikolaj Bjorner	c44c8284bd	use worklist algorithm to avoid stack overflow #1125 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-06-30 18:10:36 -07:00
Nikolaj Bjorner	9b631f982b	n/a ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-06-30 17:48:04 -07:00