7730 commits

Author	SHA1	Message	Date
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
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
Arie Gurfinkel	3af3c82f67	Normalize lit0 in theory clause	2018-06-25 09:21:30 -04: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
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
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
Nikolaj Bjorner	19e2f8c9d5	fix #1694 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-20 17:35:41 -07:00
Nikolaj Bjorner	0c32989144	change to const qualifier on constructor ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-20 15:07:21 -07:00
Nikolaj Bjorner	792bf6c10b	fix tests ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-20 08:22:15 -07:00
Nikolaj Bjorner	81e5589bc8	Merge branch 'master' of https://github.com/z3prover/z3	2018-06-19 23:23:56 -07:00
Nikolaj Bjorner	335d672bf1	fix #1675, regression in core processing in maxres ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-19 23:23:19 -07:00
Nikolaj Bjorner	8241ba784d	Merge branch 'master' of https://github.com/z3prover/z3	2018-06-19 16:33:34 -07:00
Nikolaj Bjorner	341f7ceb17	remove quantified lemmas for idiv/mod ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-19 13:19:48 -07:00
Nikolaj Bjorner	eeba30a277	fix #1677 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-19 10:56:45 -07:00
Nikolaj Bjorner	2456513053	sometimes comments are worth reading ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-19 10:43:51 -07:00
Nikolaj Bjorner	9b6a99794b	add default method for fresh fp value, try to address OsX build ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-19 10:02:31 -07:00
Nikolaj Bjorner	8a29c2803c	improvements to arithmetic preprocessing simplificaiton and axiom generation for #1683 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-19 07:04:39 -07:00
Nikolaj Bjorner	86c39c971d	fix #1681 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 21:53:45 -07:00
Nikolaj Bjorner	b4aac1ab55	revert fix to #1677 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 21:23:13 -07:00
Nikolaj Bjorner	c15eca66d6	fix #1685 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 20:53:33 -07:00
Nikolaj Bjorner	6a0b70ee5c	selective expansion of strings for canonizer to fix #1690 regression ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 20:42:53 -07:00
Nikolaj Bjorner	4634d1daed	selective expansion of strings for canonizer to fix #1690 regression ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 20:37:39 -07:00
Nikolaj Bjorner	8040eddf65	fix #1658 fix #1689 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 16:41:04 -07:00
Nikolaj Bjorner	c3b27903f8	fix #1677 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 11:22:01 -07:00
Nikolaj Bjorner	55ebf69648	move comment to fix #1682 ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 09:42:05 -07:00
Nikolaj Bjorner	cd890bd993	fix bug in order for model conversion in normalize_bounds ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-18 09:34:53 -07:00
Nikolaj Bjorner	c81f25a1c8	fix build issue ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-17 09:59:03 -07:00
Nikolaj Bjorner	035baf7cb9	align use of spaces before for/if/while ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2018-06-17 09:43:40 -07:00