Order of assumptions appears to make a huge difference on what lemmas
are discovered. Shuffling the assumptions ensures that the solver
is never stuck with any bad order.
pob_queue is a priority queue. Changing a pob while it is in the queue might change
the priority. This is a source of subtle bugs. The flag is ment to help defend
against this issues in the future.
As a side-effect, a pob that is already in the queue will be silently not added
to it, and a new version of a pob might be created if a version being looked
for is already in the queue.
Lemma inherits its weakness score from the pob. However,
pob's weakness might be reset or changed for some other reason.
To avoid affecting the lemma, the weakness is copied on
construction.
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
change in settings + random in adding terms to hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add terms in hnf from the beginning
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
adjusting settings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove non used determinant()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixex in maximize_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
prepare for LIRA (#76)
* merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* simple mixed integer example
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj's fixes in theory_lra.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes in maximize_term, disable find_cube for mixed case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix cube heuristic for the mixed case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix the build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix in find cube delta's calculation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove a printout
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove a blank line
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
test credentials
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
avoid double checks to add terms in hnf_cutter
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
fixes in add terms to hnf_cutter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove a variable used for debug only
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove a field
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove a warning and hide m_A_orig under debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use var_register to deal with mapping between external and local variables
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
tighten the loop in explain_implied_bound
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes in theory_lra and relaxing debug checks in pop(), for the case when push() has been done from not fully initialized state
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
suppress hnf cutter when the numbers become too large
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove some debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
adjusting hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
exit earlier on a large matrix in hnf_cutter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
call hnf only for the boundary points
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix a bug in hnf_cutter initialization
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
initialize has_bounds in lar_solver::get_equality_for_term_on_corrent_x
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes in determinant_of_rectangular_matrix calculations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
changes in debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
init m_hnf_cut_period from globals settings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix some warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Lev2 (#66)
* log quantifiers only if present
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* merge and fix some warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
remove a comment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify gomory cut return's logic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify uniformly int_solver::check()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
making new arith solver default for LIA (#67)
* log quantifiers only if present
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* merge and fix some warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
* set new arith as default for LIA
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
remove chase_cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove integer_domain
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
restore call for find_cube()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove a method
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove some debug code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fill the matrix A in hnf_cutter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fill the matrix A in hnf_cutter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
first steps of hnf cutter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
handle generated cases in hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
call hnf only for a full rank matrix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
get (H reversed) * b
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
finding the cut row randomly, exiting if is not there
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
produce first cuts with hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
produce first cuts with hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
define by lp_settings if to avoid calling hnf_cutter when the solution is not on the boundary
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
revert to the previous version
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work in hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work in hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work in hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work in hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
prepare calculate U in hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
naive algorithm for HNF and m <= n
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
naive algorithm for HNF
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
introduces reverse matrix into Hermite Normal Form calculation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on more efficient hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use smarter templates in lu.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
the new lu scheme compiles
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simple test passes with the modified lu
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix the build on windows
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
playing with the example from cutting the mix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf, add extended_gcd_minimal_uv()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on extended_gcd_minimal_uv
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf, add extended_gcd_minimal_uv()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
more tests and bug fixes in hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf modulo version
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf modulo version, more tests pass
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
a rough version of hnf passed the tests
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix build in release
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes in determinant calculations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on hnf
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
create a stub for hnf_cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
create a stub for hnf_cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
create a stub for hnf_cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
general_matrix etc.
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
general_matrix etc.
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
rename cut_solver to chase_cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
rename cut_solver to chase_cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
hnf_cutter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use special bounds inf find_cube for x+y, x-y
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
bug fixes in column patching, add stats to patching, restructure int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
comment out m_old_values from int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
avoid calling pivot_fixed_vars_from_basis() in int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix the return value from path_nbasic_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix the return value from path_nbasic_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work in patch_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on int_solver check()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
exit from find_free_interval() when l >= u
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
experiment with branching on nbasic columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove m_old_values
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add rounding to patch_columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
qflia
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
patch all columns, round non-patched, branch or basic columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
refactor int_solver::check()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
restore move_non_basic_columns_to_bounds() after a failure in find_cube()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
optimize gomory cuts search
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
produce gomory cuts without moving columns to bounds
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
call find_feasible_solution() after moving columns
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
alway move colums to bounds before gomory cut
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
merge from best branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
correction in the sign of gomory_cut
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix in the gomory cut sign
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
try using lemmas of cut_solver as cuts
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add find_cube() proposed by Nikolaj
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
restore m_int_branch_cut_solver to 8
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
accept empty lar_terms in theory_lra and also do not create empty lar_terms/lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
qflia_tactic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
call find_feasible solution to recover for a failure in find_cube
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
do not tighten unused terms
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
get rid of inf_int_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix a bug with an accidental solution in cube
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
get rid of inf_int_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
bug fix with has_int_var() for lar_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix in find_inf_int_base_column
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
detect slow propagations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fiddle with the stop conditions
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
get rid of constraint->m_predecessors, fix a bug in push/pop with lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
clean detection of stale lemmas in pop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add constraints lazily to cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
refactor some of cut_solver classes into include files
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
prepare to index constraint from 0 to to n - 1, where n is the number of constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
prepare for constraint priority
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use priorities in active_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove unnecesessary parameters
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
speedup bound propagations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
restore tactics
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
speedup bound propagation by avoiding some calls to propagate_constraint_only_one_unlim
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes by Nikolaj
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix print lp_core_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on gomory test, subs terms indices correctly
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
correct const_iterator for lar_term
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
improve static_matrix with iterators
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
make row_strip a struct
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
move row_strip outside of static_matrix
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add const_iterator to row_strip
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove the hierarchy of iterators - use std::iterators
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
adding gcd_test stats and taking care of for iterators
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
restore qflia_tactic.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
run gcd_test according to settings()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
experiment with picking a narrow or random branch
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
syntax errors
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
use std::vector instead of vector in cut_solver temporarily
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix in is_upper_bound, is_lower_bound
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add bound() for polynomial, needs more testing
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on resolve
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
implement resolve()
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
implement improves()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
replace low_bound by lower_bound
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
better printing in cut_solver.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add value vector to cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on bound propagaion for cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
bound propagation for integer inequalites
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
bound propagation for integer inequalites
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
bound propagattions on integers
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
adding m_explanation field to cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify bound propagation in cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
calculate conflict explanation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
change m_explanation type to a set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
making cut_solver a member of int_solver, missing push/pop support
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Nikolaj's comments
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Nikolaj's comments
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
return explanations from cut_solver and hook up push/pop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
hook up push/pop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
using resize of std::vector
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
it is a big squashed commit
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
rename hpp to cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes in push/pop of cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
return simple inequalities a part of a conflict
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on propagation and the main loop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add file
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
init m_v[j], the var values only when j is fixed
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
handle decide in cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
start on resolve_conflict
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
start on resolve_conflict
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove cut_solver_def.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
in the middle
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
change signature of resolve
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix the domain of the decided var
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on tightening of ineqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on tight ineqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
resolve conflict
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix in usage of resolve()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on conflict resolution
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
cut_solver is not a template
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
represent var_info as a class, not a struct
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
make literal a class
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
better resolve_conflict scheme, and switch to *constraints in literals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
debug conflict resolution in cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
switch to vector
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove nondetermenistic behavior from cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
debug resolve conflict
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix backjump
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix backjump
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix backjump
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix backjump
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
dumb explanation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
get rid of a parameter
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add lemmas origins
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use lemma_origins to provide correct explanations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use lemma_origins to provide correct explanations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
store lemmas in a separate vector
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use std::unordered_set for m_dependent_constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use std::unordered_set for m_dependent_constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix bugs with lemmas
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
finding conflicting cores
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
switch from changed variables to active_set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
less active constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
work on cut_solver.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
propagate simple constraing immediately
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
propagate simple constraints immediately
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixing bugs with active set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove const_cast
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
towards unbounded variables
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
toward unbounded variables
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
toward unbounded variables
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
make lemmas_origins a set
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use correct hash and equal in m_lemma_origins
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add testing code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add testing code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
debug unlimited vars
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
take in Nikolaj's comments and improvements
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
address the comments
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
handle unlimited vars in check_inconsistent
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
debug
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
detect trivial polynomials in resolve
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Nikolaj's changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify handling of m_global_bound_var
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
decide on m_global_bound_var if it is not fixed
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify m_global_bound_var
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
remove m_global_bound_var, simplify the indexing of var_infos of cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
do not run cut_solver with vars without any bound
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
small changes
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add cancellation in cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
do not pop lemmas during a cut_solver run
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
treating cut_solver as an heurisitic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
prepare for cut_solver returning undef
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify work with active_set in cut_solver, add stats
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify var_info literals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix a bug in fill_conflict_explanation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix a bug in the conflict explanation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add timeout to validate_* in theory_lra.cpp
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify cut_solver, no special treatment for simple constraints
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
cleanup the cancel story
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
cleanup cancelling
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix a bug in push/pop of cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
extract a method in int_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
some progress with the new scheme
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
add testing code
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes in test and in literal creation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix a bug in bound propagation in cut_solver.h
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
simplify cut_solver
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
provide valid conflict explanation
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use a lazy push in stacked_map
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use a lazy push in stacked_map
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
optimize stack operations on var_info's domains
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fix a bug in tightening
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
use the standard tactics from qflia_tactic
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
spread the var domain stack over literals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
spread the var domain stack over literals
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
avoid cycling in cut_solver.h and fixes in push/pop
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
fixes after rebase
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
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>
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()
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>
