708 commits

Author	SHA1	Message	Date
Nikolaj Bjorner	fe1a07a8ee	merge ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-27 16:17:56 -07:00
Christoph M. Wintersteiger	33ebdc8adc	Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872.	2017-07-27 23:08:35 +01:00
Nikolaj Bjorner	6558999cef	fixes #1171 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-27 08:46:20 -07:00
Nikolaj Bjorner	b1298d7bde	ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-26 20:28:55 -07:00
Nikolaj Bjorner	9f9c575451	fix bug exposed when running test-z3.exe /a in debug mode, #1159. Add assertions to heap interaction ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-25 16:26:45 -07:00
Christoph M. Wintersteiger	75b533f050	Fixed normalization shift in MPF rounder. Relates to #872.	2017-07-25 20:29:10 +01:00
Christoph M. Wintersteiger	f1c0ac72e7	Fix for fp.fma encoding. Relates to #872.	2017-07-25 20:29:10 +01:00
Nikolaj Bjorner	70f6280bf1	fix regression reported in #1159 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-25 10:18:21 -07:00
Nikolaj Bjorner	a94f5fb04a	fix compiler warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-24 12:15:10 -07:00
Nikolaj Bjorner	30b0d5ba13	Merge branch 'master' of https://github.com/z3prover/z3	2017-07-24 10:49:54 -07:00
Lev Nachmanson	bd4fb22665	track the set of integer variables that are not set to integer values ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-21 21:09:51 -07:00
Lev Nachmanson	64e542bd70	fix term indices for the time being when exiting from check() ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-20 19:13:13 -07:00
Lev Nachmanson	04824e7372	add a check in gomory cut ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-20 18:12:16 -07:00
Lev Nachmanson	1490b7a15f	a cleaner version of subs_term_columns ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-19 22:14:05 -07:00
Lev Nachmanson	4d1b0d8026	gomory cut worked on a toy example ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-19 16:50:23 -07:00
Lev Nachmanson	94b3fee6ac	rename a function ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-17 16:41:02 -07:00
Lev Nachmanson	729644a2b6	fix term_is_int ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-17 16:08:20 -07:00
Lev Nachmanson	77171f4af8	the first version of Gomory cut, probably broken ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-17 15:17:46 -07:00
Lev Nachmanson	1931adcb74	add a file ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-13 09:48:29 -07:00
Lev Nachmanson	8750da1da7	progress in gomory cut ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-12 16:43:10 -07: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	fc6a876845	start gomory cut ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-07-11 13:38:59 -07: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
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
Lev Nachmanson	3abc793876	solve more integer smt problems	2017-07-07 11:47:52 -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	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	253870c6d7	fix compiler warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-07-04 13:08:23 -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	9b631f982b	n/a ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-06-30 17:48:04 -07:00
Nikolaj Bjorner	a28a8304b7	Dev (#56) ... * 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>	2017-06-28 13:12:12 -07:00
Lev Nachmanson	dfe15adf7e	fix maybe non initialized warning ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-06-26 16:32:44 -07:00
Nikolaj Bjorner	7db1847f51	fix bitrot in maxsat example reference management #1116 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-06-26 09:36:53 -07:00
Christoph M. Wintersteiger	2fceac04d4	Merge branch 'master' of https://github.com/Z3Prover/z3	2017-06-25 22:19:54 +01:00
Christoph M. Wintersteiger	c395516058	Adjusted rlimit increments in theory_arith to avoid non-termination issues	2017-06-25 22:19:42 +01:00
Nikolaj Bjorner	5752830f71	bug fixes ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-06-22 15:01:12 -07:00
Lev Nachmanson	2a5f1d6e93	add a template instantination ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-06-22 10:32:35 -07:00
Nikolaj Bjorner	5e2f7f7177	fixes top lookahead simplification ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-06-21 20:22:31 -07:00
Dan Liew	d00892c9a6	[CMake] Fix dependencies for generating mem_initializer.cpp. ... Previously CMake was not aware of which headers files the generation of `mem_initializer.cpp` depended on. Consequently this could result in broken incremental builds if * Existing headers that declare memory initializers/finalizers change. * New headers are added that declare memory initializers/finalizer. Now the `z3_add_component()` CMake function has been modifed so that it now takes an optional `MEMORY_INIT_FINALIZER_HEADERS` argument which allows the headers that declare memory initializers/finalizers to be explicitly listed. With this information CMake will now regenerate `mem_initializer.cpp` correctly. This required the `mk_mem_initializer_cpp_internal()` function to be changed to take a list of header files rather than a list of component source directories. The two consumers (CMake and Python/Makefile build systems) of this function have been modified to work with this change. This partially fixes #1030.	2017-06-21 23:56:53 +01:00
Dan Liew	6f48a145aa	[CMake] Fix dependencies for generating gparams_register_modules.cpp. ... Previously CMake was not aware of which headers files the generation of `gparams_register_modules.cpp` depended on. Consequently this could result in broken incremental builds if * Existing headers that declared module description/parameters change. * New headers are added that declare module description/parameters. * `.pyg` files that generate header files that declare module description/parameters change Now the `z3_add_component()` CMake function has been modifed so that * All header files that are generated from `.pyg` files are added as dependencies and are scanned from module description/parameter declarations. This implicit dependency of `gparams_register_modules.cpp` depending on other generated header files seems unnecessary complex. We should revisit this design decision once the Python/Makefile build system is deprecated. * The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS` argument which allows the headers that declare module description/paramters to be explicitly listed. With this information CMake will now regenerate `gparams_register_modules.cpp` correctly. This required the `mk_gparams_register_modules_internal()` function to be changed to take a list of header files rather than a list of component source directories. The two consumers (CMake and Python/Makefile build systems) of this function have been modified to work with this change. This partially fixes #1030.	2017-06-21 23:56:46 +01:00