From ccb50f5d8a6459246792c9c469514de9c2fbbb9c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 19 Oct 2012 08:33:43 -0700 Subject: [PATCH] updated comments to create_children Signed-off-by: Nikolaj Bjorner --- lib/pdr_context.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/lib/pdr_context.cpp b/lib/pdr_context.cpp index 53cc9aac5..b24c6fa1c 100644 --- a/lib/pdr_context.cpp +++ b/lib/pdr_context.cpp @@ -1674,24 +1674,16 @@ namespace pdr { - T(x0,x1,x) for transition - phi(x) for n.state() - - psi(x0,x1,x) for psi - M(x0,x1,x) for n.model() Assumptions: - M => psi - psi => phi & T - psi & M agree on which rules are taken. + M => phi & T In other words, - 1. psi is a weakening of M - 2. phi & T is implied by psi + 1. phi & T is implied by M Goal is to find phi0(x0), phi1(x1) such that: - phi(x) & phi0(x0) & phi1(x1) => psi(x0, x1, x) - - or at least (ignoring psi alltogether): - phi(x) & phi0(x0) & phi1(x1) => T(x0, x1, x) Strategy: