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>
