From 9fb4e4a343ce4104258affb9a38d5999307fe588 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Fri, 3 Mar 2017 20:08:06 +0100 Subject: [PATCH] encoder --- logics/rsltl.py | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/logics/rsltl.py b/logics/rsltl.py index a83ecb0..e4fb04b 100644 --- a/logics/rsltl.py +++ b/logics/rsltl.py @@ -125,5 +125,10 @@ class Formula_rsLTL(object): #x = ~( FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent1") == 3) | (BagDescription.f_entity("ent2") < 3)) ) ) ) & FormulaLTL.f_X(BagDescription.f_TRUE(), FormulaLTL.f_bag( ~((BagDescription.f_entity("ent3") == 1) ) ) ) #print(x) - - +class Encoder_rsLTL(object): + """Class for encoding rsLTL formulae for a given smt_checker instance""" + + def __init__(self, smt_checker): + self.smt_checker = smt_checker + +