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
trinhmt
54a9482716
Merge pull request #8 from Z3Prover/master
...
merge with Z3Prover/z3
2018-06-27 18:10:54 +08:00
Nuno Lopes
2b31024dab
add obj_ref::operator=(obj_ref &&) + a few explicit uses
2018-06-26 17:00:56 +01:00
Nikolaj Bjorner
520ce9a5ee
integrate lambda expressions
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-26 07:23:04 -07:00
Thai Trinh
aacb7289be
merge with Z3Prover/master
2018-06-25 19:44:46 +08:00
Nikolaj Bjorner
9149048f34
use quotes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-15 15:53:47 -07:00
Nikolaj Bjorner
c0e378b045
remove {
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-15 15:44:33 -07:00
Arie Gurfinkel
3ad1446597
Remove spurious quote
2018-06-15 15:09:25 -07:00
Nikolaj Bjorner
6fc08e9c9f
Merge branch 'master' of https://github.com/z3prover/z3
2018-06-15 14:58:10 -07:00
Nikolaj Bjorner
a51d6cbcbc
debug model evaluator
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-15 14:58:02 -07:00
Nikolaj Bjorner
7714d05c1a
fill out qe_solve_plugin functionality
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-14 16:08:52 -07:00
Nikolaj Bjorner
4547f2c001
enable non-expression bodies of quantifiers to fix #1667
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-07 22:03:03 -07:00
Nikolaj Bjorner
88ead235f0
gcc mode
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 19:30:56 -07:00
Nikolaj Bjorner
bb53060313
int64_t
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 19:26:40 -07:00
Nikolaj Bjorner
8565de2c5b
deal with shift exponent error
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 19:17:37 -07:00
Nikolaj Bjorner
ad67424987
deal with shift exponent error
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 18:23:04 -07:00
Nikolaj Bjorner
99bdb46158
int64_t
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 17:48:30 -07:00
Nikolaj Bjorner
8ab428b660
try new gcd
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-06-06 17:42:44 -07:00
Nikolaj Bjorner
d088a1b9f6
updated release notes for merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 18:25:14 -07:00
Nikolaj Bjorner
0708ecb543
dealing with compilers that don't take typename in non-template classes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 09:11:33 -07:00
Nikolaj Bjorner
2800049dd4
stale files
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-23 08:49:49 -07:00
Nikolaj Bjorner
50c93d1ad4
merge with 4.7.1
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-22 17:10:36 -07:00
Nikolaj Bjorner
6938c76950
Merge pull request #1630 from danielschemmel/warnings
...
Fix GCC Warnings
2018-05-20 10:24:05 -07:00
Daniel Schemmel
1cc4a4ccc5
remove unused constructor that would construct lar_constraint in an partly initialized state. Fixes: variable may be used uninitialized
2018-05-19 02:56:46 +02:00
Nikolaj Bjorner
d462ed3f00
fix #1621
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-18 14:30:27 -07:00
Nikolaj Bjorner
925867dc3e
fix #1621
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-18 14:14:00 -07:00
Daniel Schemmel
2d5dd80238
The Permutation Matrix' values function attempted an incorrect conversion.
...
This causes compilation with GCC 8 to fail. I suspect it worked previously due to SFINAE.
2018-05-07 23:33:40 +02:00
Nikolaj Bjorner
13b54f379c
fix ema
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-05 13:58:47 +02:00
Nikolaj Bjorner
43403fafcd
adding ema
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-03 13:23:59 -07:00
Nikolaj Bjorner
dd6e76478d
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-02 08:51:33 -07:00
Nikolaj Bjorner
c2bf8ef410
resolve
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 15:03:15 -07:00
Nikolaj Bjorner
a07c6e4793
resolve
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 15:02:04 -07:00
Nikolaj Bjorner
e4d24fd2c3
fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 09:39:19 -07:00
Nikolaj Bjorner
5ba814b14f
try string in pragma
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 08:54:05 -07:00
Nikolaj Bjorner
42c9394c6d
pragma
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 08:49:48 -07:00
Nikolaj Bjorner
812c913cdd
use C99 pragma
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 08:34:28 -07:00
Nikolaj Bjorner
78b9f0686a
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 07:43:29 -07:00
Nikolaj Bjorner
f525f43e43
merge
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-30 09:30:43 -07:00
Nikolaj Bjorner
859c68c2ac
merge with opt
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-30 08:27:54 -07:00
