10084 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Nikolaj Bjorner	91ef84b8c9	Merge branch 'master' of https://github.com/z3prover/z3	2018-06-27 11:25:04 -07:00
Nikolaj Bjorner	20fc573d5b	add laxer check for oeq_quant_intro ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-27 11:24:56 -07:00
Lev Nachmanson	58ca4518e5	clean up int_solver ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add a diagnostic method Signed-off-by: Lev Nachmanson <levnach@hotmail.com> white space change Signed-off-by: Lev Nachmanson <levnach@microsoft.com> cleanup in int_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> some cleanup Signed-off-by: Lev Nachmanson <levnach@microsoft.com> remove m_became_zeros Signed-off-by: Lev Nachmanson <levnach@microsoft.com> start cut_solver, work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> start cut_solver, work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> workin on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> working on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> working on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> working on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix bugs in disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix bugs in gisjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix bugs in gisjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix bugs in disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix bugs in disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix bugs is disjoint intervals Signed-off-by: Lev Nachmanson <levnach@microsoft.com> bug fixes in disjoint_intervals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> disjoint_intervals passes the test Signed-off-by: Lev Nachmanson <levnach@hotmail.com> test disjoint_intervals push(), pop() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2018-06-27 10:53:03 -07:00
Lev Nachmanson	db8f01894f	solve send-more-money_lev.smt2 ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com> handle integer vars in random_update Signed-off-by: Lev Nachmanson <levnach@microsoft.com> call the assert in gomory_cut and branching to a correct place Signed-off-by: Lev Nachmanson <levnach@microsoft.com> fixes in goromy cut Signed-off-by: Lev Nachmanson <levnach@microsoft.com> disable x values tracking in random_update Signed-off-by: Lev Nachmanson <levnach@microsoft.com> more fixes in gomory cut Signed-off-by: Lev Nachmanson <levnach@microsoft.com> change in mk_bound by Nikolaj Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in gomory cut and setup Signed-off-by: Lev Nachmanson <levnach@microsoft.com> fixes in int_solver Signed-off-by: Lev Nachmanson <levnach@microsoft.com> change a printout Signed-off-by: Lev Nachmanson <levnach@microsoft.com> fix by Nikolaj in treating terms returned by int_solver Signed-off-by: Lev Nachmanson <levnach@microsoft.com> fix syntax Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix a free coefficient bug in bound propagaion and simplify gomory cut Signed-off-by: Lev Nachmanson <levnach@microsoft.com> avoid tracking pivoted rows during int_solver::check()	2018-06-27 10:49:20 -07:00
Lev Nachmanson	aba7dcab3e	fix a bug in the lar_solver::m_status update during push/pop ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com> progress in gomory cut Signed-off-by: Lev Nachmanson <levnach@microsoft.com> the first version of Gomory cut, probably broken Signed-off-by: Lev Nachmanson <levnach@microsoft.com> rename a function Signed-off-by: Lev Nachmanson <levnach@microsoft.com> gomory cut worked on a toy example Signed-off-by: Lev Nachmanson <levnach@microsoft.com> track the set of integer variables that are not set to integer values Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2018-06-27 10:19:06 -07:00
Lev Nachmanson	0164ea9abb	change the order of initializations in the constructor of imp in theory_lra ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2018-06-27 10:09:29 -07:00
Lev Nachmanson	e1d3119f9f	use a faster version of get_model in debug checks ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2018-06-27 10:09:29 -07:00
Lev Nachmanson	2e957a97cf	replace clp to clean ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2018-06-27 10:09:29 -07:00
Lev Nachmanson	d41c65a4f9	replace lean to lp ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2018-06-27 10:09:23 -07:00
Lev Nachmanson	db0a3f4358	solve all smt2 from QF_LIA/calypto with int_solver ... Signed-off-by: Lev Nachmanson <levnach@microsoft.com>	2018-06-27 10:08:07 -07:00
Lev Nachmanson	a52c33a3e1	solve more ilp smt ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2018-06-27 10:06:39 -07:00
Nikolaj Bjorner	281882e3b1	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>	2018-06-27 10:05:19 -07:00
Lev Nachmanson	9eb82815e2	fix a bug in pivot_fixed_vars_from_basis ... Signed-off-by: Lev Nachmanson <levnach@hotmail.com>	2018-06-27 10:05:19 -07:00
Nikolaj Bjorner	8bd029c657	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>	2018-06-27 10:05:19 -07:00
Nikolaj Bjorner	c82aa5edce	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>	2018-06-27 10:04:46 -07:00
Nikolaj Bjorner	06c9a9f3e1	merge ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-27 08:51:22 -07:00
Nikolaj Bjorner	5762be2a0f	fix 1703 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-27 08:49:52 -07:00
trinhmt	54a9482716	Merge pull request #8 from Z3Prover/master ... merge with Z3Prover/z3	2018-06-27 18:10:54 +08:00
Thai Trinh	1892d31794	add parameter to enable splitting guided by length constraints	2018-06-27 18:10:40 +08:00
Nuno Lopes	6c64e138b0	ufbv_rewriter_tactic: remove unneeded imp class	2018-06-26 18:05:14 +01:00
Nuno Lopes	2b31024dab	add obj_ref::operator=(obj_ref &&) + a few explicit uses	2018-06-26 17:00:56 +01:00
Nikolaj Bjorner	ea4218a192	add upper-case files ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-26 07:52:38 -07:00
Nikolaj Bjorner	1c1357af7d	remove lower case files ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-26 07:52:02 -07:00
Nikolaj Bjorner	a8e864a3e6	add missing files ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-26 07:36:36 -07:00
Nikolaj Bjorner	520ce9a5ee	integrate lambda expressions ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-26 07:23:04 -07:00
Nikolaj Bjorner	bf4edef761	fix mbi arithmetic solver for lower bounds ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-26 06:37:47 -07:00
Nikolaj Bjorner	6804329661	Merge pull request #1701 from agurfinkel/deep_space ... Normalize lit0 in theory clause	2018-06-25 07:35:34 -07:00
Arie Gurfinkel	3af3c82f67	Normalize lit0 in theory clause	2018-06-25 09:21:30 -04:00
Thai Trinh	69f92a309f	Merge branch 'Z3Prover-master'	2018-06-25 20:16:38 +08:00
Thai Trinh	613ff53821	Merge branch 'master' of https://github.com/Z3Prover/z3 into Z3Prover-master ... Conflicts: src/smt/theory_seq.cpp src/smt/theory_seq.h	2018-06-25 20:16:09 +08:00
Thai Trinh	aacb7289be	merge with Z3Prover/master	2018-06-25 19:44:46 +08:00
Nikolaj Bjorner	a5f4980c92	Merge pull request #1700 from agurfinkel/deep_space ... Deep space	2018-06-24 19:13:34 -07:00
Arie Gurfinkel	f330b96a35	Gracefully failing in assign-bounds to farkas	2018-06-24 21:03:09 -04:00
Arie Gurfinkel	e906930922	Debug code	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	8e57ab5d97	Computing missing coeff for assign-bounds lemma	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	1764bb8785	Cleaning up unsat_core_learner	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	7b2ca769ef	Cleanup	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	58dc5451e1	iuc code cleanup	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	9c9d0d0840	convert assign-bounds axioms to farkas lemmas	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	ac23002dce	Fix bugs in iuc generation	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	4ed6783aff	Formatting only. No change to code	2018-06-24 20:43:04 -04:00
Arie Gurfinkel	fcfa6baeca	Refactor mk_th_lemma	2018-06-24 20:43:04 -04:00
Nikolaj Bjorner	915983821b	add rewrite to each branch of mbp ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-24 17:06:49 -07:00
Nikolaj Bjorner	c32bfb5ecd	fix crash during cancelation ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-24 15:29:40 -07:00
nilsbecker	4f64f069ab	Merge remote-tracking branch 'upstream/master'	2018-06-24 08:08:32 +02:00
Nikolaj Bjorner	61c25fdc8e	Merge branch 'master' of https://github.com/z3prover/z3	2018-06-23 21:57:19 -07:00
Nikolaj Bjorner	e187023304	fix #1699 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-23 21:57:10 -07:00
Nikolaj Bjorner	3d27232b2a	Merge pull request #1697 from rainoftime/master ... Refine default_tactic for better support of pure SAT instances	2018-06-22 09:31:19 -07:00
rainoftime	fc8b1d9a7d	Refine default_tactic: if the constraint is an SAT instance and proof is not enabled, then use the qffd tactic	2018-06-22 16:46:47 +08:00
Nikolaj Bjorner	8969a7035c	Merge pull request #1693 from NikolajBjorner/master ... fix #1675	2018-06-20 17:36:24 -07:00