Replace assertions/hypotheses of aux variables with PR_TRUE.
Rebuild unit resolution as needed.
This makes the transformation stable against new proof rules.
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>
