mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

add comments to generalizer code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-09 09:00:40 -07:00
parent 85391b6f35
commit cb06ce295e
1 changed files with 12 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/muz_qe/pdr_generalizers.cpp
View file

@ -162,6 +162,18 @@ namespace pdr {
}
// use the entire region as starting point for generalization.
//
// Constraints:
// add_variables: y = y1 + y2
// core: Ay <= b -> conv1: A*y1 <= b*sigma1
// sigma1 > 0
// sigma2 > 0
// 1 = sigma1 + sigma2
// A'y <= b' -> conv2: A'*y2 <= b'*sigma2
//
// If Constraints & Transition(y0, y) is unsat, then
// update with new core.
//
void core_convex_hull_generalizer::method1(model_node& n, expr_ref_vector& core, bool& uses_level) {
manager& pm = n.pt().get_pdr_manager();
expr_ref_vector conv1(m), conv2(m), core1(m), core2(m), eqs(m);