From 1b94cbc7c00b26327ca806cc6fd4a7db12b0eafb Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 5 Nov 2017 17:52:02 +0000 Subject: [PATCH] Loading of the variables to use for the encoding --- logics/rsltl_encoder.py | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py index 79844b8..c1f61e7 100644 --- a/logics/rsltl_encoder.py +++ b/logics/rsltl_encoder.py @@ -8,16 +8,34 @@ class rsLTL_Encoder(object): def __init__(self, smt_checker): self.smt_checker = smt_checker - self.v = smt_checker.v - self.v_ctx = smt_checker.v_ctx self.rs = smt_checker.rs - self.loop_position = smt_checker.loop_position + + self.v = None + self.v_ctx = None + self.loop_position = None + + # self.load_variables( + # var_rs=smt_checker.v, + # var_ctx=smt_checker.v_ctx, + # var_loop_pos=smt_checker.loop_position) self.init_ncalls() + + def load_variables(self, var_rs, var_ctx, var_loop_pos): + + self.v = var_rs + self.v_ctx = var_ctx + self.loop_position = var_loop_pos def get_encoding(self, formula, bound): + + assert self.v is not None + assert self.v_ctx is not None + assert self.loop_position is not None + self.cache_init(bound) self.init_ncalls() + return self.encode(formula, 0, bound) def init_ncalls(self):