563 commits

Author	SHA1	Message	Date
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	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
Lev Nachmanson	2a5f1d6e93	add a template instantination ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-06-22 10:32:35 -07:00
Dan Liew	4b517b96df	[CMake] Move CMake files into their intended location so the ... `contrib/cmake/bootstrap.py` script no longer needs to be executed. The previous location of the CMake files was a compromise proposed by @agurfinkel in #461. While this has served us well (allowing progress to be made) over time limitations of this approach have appeared. The main problem is that doing many git operations (e.g. pull, rebase) means the CMake files don't get updated unless the user remembers to run the script. This can lead to broken and confusing build system behaviour. This commit only does the file moving and necessary changes to `.gitignore`. Other changes will be done in subsequent commits.	2017-06-12 11:59:00 +01:00
Nikolaj Bjorner	c28f26c17d	merge and update ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-25 14:17:19 -07:00
Nikolaj Bjorner	e306287d7b	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>	2017-05-25 14:04:48 -07:00
Nikolaj Bjorner	d2b2aedef3	Merge branch 'dev' of https://github.com/nikolajbjorner/z3	2017-05-25 08:54:00 -07:00
Lev Nachmanson	73e919c002	test ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-24 17:31:17 -07:00
Nikolaj Bjorner	b18dc7d052	adding nra ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-24 17:24:36 -07:00
Nikolaj Bjorner	4726d32e2f	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>	2017-05-24 16:32:14 -07:00
Nikolaj Bjorner	7a809fe4f0	adding nra solver ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-24 14:56:59 -07:00
Nikolaj Bjorner	80bb084611	add missing initialization ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-24 14:47:09 -07:00
Nikolaj Bjorner	d45c56da3f	adding nra solver ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-24 14:44:16 -07:00
Nikolaj Bjorner	fc53c5b638	adding nra solver ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-24 14:41:02 -07:00
Lev Nachmanson	09530bb6bc	adding some content to the new check_int_feasibility() ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-24 10:12:42 -07:00
Nikolaj Bjorner	dcc6284557	adding constraints ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-24 08:57:10 -07:00
Nikolaj Bjorner	b9ca8b435f	nlsat integration ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-23 20:45:58 -07:00
Nikolaj Bjorner	e231f4bc87	adding more nlsat ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-23 18:50:18 -07:00
Lev Nachmanson	93a3c486b0	small fix in lar_solver.cpp ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-23 18:32:08 -07:00
Nikolaj Bjorner	8ecd8a2a52	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>	2017-05-23 18:07:58 -07:00
Nikolaj Bjorner	db54cab8b2	initial skeletons for nra solver ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-23 16:26:46 -07:00
Nikolaj Bjorner	f1ca1de408	initial skeletons for nra solver ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-23 16:12:46 -07:00
Lev Nachmanson	1f425824ff	adding stub check_int_feasibility() ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-23 15:46:53 -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	2834fea9b3	fix x64 warnings ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-23 08:58:21 -07:00
Lev Nachmanson	1b62592015	change in a comment ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-18 13:44:00 -07:00
Lev Nachmanson	21bddd94bf	after merge with Z3Prover ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-18 13:28:32 -07:00
Lev Nachmanson	942f8f8c49	merge ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-18 13:18:16 -07:00
Nikolaj Bjorner	79a8e9aab0	fix build break #1029 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-18 12:09:51 -07:00
Lev Nachmanson	b92f0acae3	fix add_constraint and substitute_terms_in_linear_expression ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-18 10:56:50 -07:00
Lev Nachmanson	e9d9354885	add_constraint has got a body ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-17 19:00:33 -07:00
Lev Nachmanson	9a58eb63cb	resurrect lp_tst in its own director lp ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-17 11:01:04 -07:00
Nikolaj Bjorner	4069e76ab0	remove unused column function field, #1021 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-16 21:27:43 -07:00
Lev Nachmanson	d5e06303ef	add queries for integrality of vars ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-16 17:54:09 -07:00
Lev Nachmanson	7b433bee2b	track which var is an integer ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-16 17:36:32 -07:00
Lev Nachmanson	06e1151ca0	add int_solver class ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-16 12:01:16 -07:00
Lev Nachmanson	4eec8cbadd	introduce int_solver.h ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2017-05-15 15:32:31 -07:00
Lev Nachmanson	07f2fd43bb	Merge remote-tracking branch 'upstream/master'	2017-05-11 17:49:33 -07:00
Lev Nachmanson	d0d71a0907	allow more failures in d_solver ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-11 17:49:27 -07:00
Nikolaj Bjorner	a9e2a1204e	add this qualifier for build ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-11 16:58:29 -07:00
Nikolaj Bjorner	7b35eacf63	add this qualifier for build ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-11 16:52:54 -07:00
Nikolaj Bjorner	2ab0f281f3	add this qualifier for build ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-11 16:50:39 -07:00
Nikolaj Bjorner	29a49f4427	convert static random fields to non-static ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-11 16:46:07 -07:00
Lev Nachmanson	cf8b35a6f3	fix init reorder warning ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2017-05-11 10:54:18 -07:00
Nikolaj Bjorner	431feab1bf	fix build warnings part 8 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-11 09:37:01 -07:00
Nikolaj Bjorner	7e004fe331	fix build warnings part 7, disable LRA for regression t201.smt2 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-11 09:28:59 -07:00
Nikolaj Bjorner	49d2b86d35	fix build warnings part 6 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2017-05-11 08:57:17 -07:00