From 81b1ab45076780a5e453fa47464ef89412fe3cae Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Fri, 22 Sep 2017 21:22:38 +0200
Subject: [PATCH] Command line arguments

---
 rs_testing.py                |  9 +++++----
 rssmt.py                     | 18 +++++++++++++++---
 smt/smt_checker_rsc_param.py |  9 +++++++--
 3 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/rs_testing.py b/rs_testing.py
index 8511320..b0ac971 100644
--- a/rs_testing.py
+++ b/rs_testing.py
@@ -5,7 +5,7 @@ from logics import *
 import sys
 import resource
 
-def run_tests():
+def run_tests(cmd_args):
     
     # test_extended_automaton()
     # process()
@@ -13,7 +13,7 @@ def run_tests():
     # scalable_chain(print_system=True)
     # example44()
     # example44_param()
-    simple_param()
+    simple_param(cmd_args)
 
 def trivial_param():
 
@@ -47,7 +47,7 @@ def trivial_param():
     smt_rsc.check_rsltl(formula=f1, max_level=10, print_witness=True)
 
 
-def simple_param():
+def simple_param(cmd_args):
 
     r = ReactionSystemWithConcentrationsParam()
     r.add_bg_set_entity(("x", 3))
@@ -72,7 +72,8 @@ def simple_param():
 
     rc = ReactionSystemWithAutomaton(r, c)
     rc.show()
-    smt_rsc = SmtCheckerRSCParam(rc, optimise=True)
+    
+    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
 
     f1 = Formula_rsLTL.f_F(
         BagDescription.f_TRUE(),
diff --git a/rssmt.py b/rssmt.py
index 05cca65..c3a1126 100755
--- a/rssmt.py
+++ b/rssmt.py
@@ -6,6 +6,8 @@
 
 """
 
+import argparse
+
 from rs import *
 from smt import *
 import sys
@@ -14,10 +16,11 @@ import rs_testing
 
 from colour import *
 
-import resource
-
 profiling = False
 
+if profiling:
+    import resource
+
 ##################################################################
 
 version = "2017/04/08/00"
@@ -43,8 +46,17 @@ def print_banner():
 def main():
     """Main function"""
 
+    parser = argparse.ArgumentParser()
+
+    parser.add_argument("-v", "--verbose", 
+        help="turn verbosity on", action="store_true")
+    parser.add_argument("-o", "--optimise", 
+        help="minimise the parametric computation result", action="store_true")
+
+    args = parser.parse_args()
+
     print_banner()
-    rs_testing.run_tests()
+    rs_testing.run_tests(args)
 
 ##################################################################
 
diff --git a/smt/smt_checker_rsc_param.py b/smt/smt_checker_rsc_param.py
index 77a3683..2b6a005 100644
--- a/smt/smt_checker_rsc_param.py
+++ b/smt/smt_checker_rsc_param.py
@@ -726,12 +726,17 @@ class SmtCheckerRSCParam(object):
         return loop_enc
     
     def solver_add(self, expression):
+        """
+        This is a solver.add() wrapper
+        """
+    
+        if expression == True:
+            return
     
         if expression == False:
             raise RuntimeError("Trying to assert False.")
         
-        if not (expression == True):
-            self.solver.add(expression)
+        self.solver.add(expression)
 
     def check_reachability(self, state, print_witness=True, 
             print_time=True, print_mem=True, max_level=1000):