Merge pull request #57 from randriu/init-optimized

optimizing formulae costruction in ColoringSmt

Author: randriu

paynt/quotient/mdp.py

@@ -459,6 +459,7 @@ def reset_tree(self, depth, enable_harmonization=True):
             self.quotient_mdp.state_valuations, self.state_is_relevant_bv,
             variable_name, variable_domain, tree_list, enable_harmonization
         )
+        # return
         self.coloring.enableStateExploration(self.quotient_mdp)
 
         # reconstruct the family

paynt/synthesizer/decision_tree.py

@@ -205,6 +205,7 @@ def map_scheduler(self, scheduler_choices):
                 break
 
     def run(self, optimum_threshold=None):
+        # self.quotient.reset_tree(SynthesizerDecisionTree.tree_depth,enable_harmonization=True)
         scheduler_choices = None
         if SynthesizerDecisionTree.scheduler_path is None:
             paynt_mdp = paynt.models.models.Mdp(self.quotient.quotient_mdp)
@@ -278,6 +279,7 @@ def run(self, optimum_threshold=None):
 
             if self.export_synthesis_filename_base is not None:
                 self.export_decision_tree(self.best_tree, self.export_synthesis_filename_base)
+
         time_total = round(paynt.utils.timer.GlobalTimer.read(),2)
         logger.info(f"synthesis finished after {time_total} seconds")
 

payntbind/src/synthesis/quotient/ColoringSmt.cpp

@@ -28,6 +28,7 @@ ColoringSmt<ValueType>::ColoringSmt(
     solver(ctx), harmonizing_variable(ctx), enable_harmonization(enable_harmonization) {
 
     timers[__FUNCTION__].start();
+    timers["ColoringSmt::0"].start();
 
     for(uint64_t state = 0; state < numStates(); ++state) {
         for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) {
@@ -60,17 +61,6 @@ ColoringSmt<ValueType>::ColoringSmt(
         STORM_LOG_THROW(variable_found, storm::exceptions::UnexpectedException, "Unexpected variable name.");
     }
 
-    // create substitution variables
-    z3::expr_vector state_substitution_variables(ctx);
-    z3::expr_vector choice_substitution_variables(ctx);
-    for(auto const& name: variable_name) {
-        z3::expr variable = ctx.int_const(name.c_str());
-        state_substitution_variables.push_back(variable);
-        choice_substitution_variables.push_back(variable);
-    }
-    z3::expr action_substitution_variable = ctx.int_const("act");
-    choice_substitution_variables.push_back(action_substitution_variable);
-
     // create the tree
     uint64_t num_nodes = tree_list.size();
     this->num_actions = *std::max_element(choice_to_action.begin(),choice_to_action.end())+1;
@@ -81,13 +71,12 @@ ColoringSmt<ValueType>::ColoringSmt(
             "Inner node has only one child."
         );
         if(child_true != num_nodes) {
-            tree.push_back(std::make_shared<InnerNode>(node,ctx,this->variable_name,this->variable_domain,state_substitution_variables));
+            tree.push_back(std::make_shared<InnerNode>(node,ctx,this->variable_name,this->variable_domain));
         } else {
-            tree.push_back(std::make_shared<TerminalNode>(node,ctx,this->variable_name,this->variable_domain,this->num_actions,action_substitution_variable));
+            tree.push_back(std::make_shared<TerminalNode>(node,ctx,this->variable_name,this->variable_domain,this->num_actions));
         }
     }
     getRoot()->createTree(tree_list,tree);
-
     getRoot()->createHoles(family);
     harmonizing_variable = ctx.int_const("__harm__");
     getRoot()->createPaths(harmonizing_variable);
@@ -118,14 +107,15 @@ ColoringSmt<ValueType>::ColoringSmt(
             STORM_LOG_THROW(domain_option_found, storm::exceptions::UnexpectedException, "Hole option not found.");
         }
     }
+    timers["ColoringSmt::0"].stop();
 
     // create choice colors
-    timers["ColoringSmt:: create choice colors"].start();
+    timers["ColoringSmt::1 create choice colors"].start();
+    // std::cout << "ColoringSmt::1 create choice colors" << std::endl << std::flush;
 
     for(std::vector<bool> const& path: getRoot()->paths) {
         path_action_hole.push_back(getRoot()->getPathActionHole(path));
     }
-
     choice_path_label.resize(numChoices());
     for(uint64_t state: state_is_relevant) {
         for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) {
@@ -136,111 +126,121 @@ ColoringSmt<ValueType>::ColoringSmt(
         }
     }
 
-    std::vector<z3::expr_vector> state_path_expression;
+    std::vector<const TerminalNode*> terminals;
+    for(uint64_t path = 0; path < numPaths(); ++path) {
+        terminals.push_back(getRoot()->getTerminal(getRoot()->paths[path]));
+    }
+
+    // allocate array for path expressions
+    uint64_t longest_path = 0;
+    for(uint64_t path = 0; path < numPaths(); ++path) {
+        longest_path = std::max(longest_path,getRoot()->paths[path].size());
+    }
+    z3::expr_vector state_valuation_int(ctx);
+    z3::array<Z3_ast> clause_array(longest_path-1+num_actions);
+
+    getRoot()->substituteActionExpressions();
+    choice_path_expresssion.resize(numChoices());
     for(uint64_t state = 0; state < numStates(); ++state) {
-        state_path_expression.push_back(z3::expr_vector(ctx));
         if(not state_is_relevant[state]) {
             continue;
         }
-        getRoot()->createPrefixSubstitutions(state_valuation[state]);
-        for(uint64_t path = 0; path < numPaths(); ++path) {
-            z3::expr_vector evaluated(ctx);
-            getRoot()->substitutePrefixExpression(getRoot()->paths[path], evaluated);
-            state_path_expression[state].push_back(z3::mk_or(evaluated));
-        }
-    }
-    std::vector<z3::expr_vector> action_path_expression;
-    for(uint64_t action = 0; action < this->num_actions; ++action) {
-        action_path_expression.push_back(z3::expr_vector(ctx));
-        for(uint64_t path = 0; path < numPaths(); ++path) {
-            z3::expr evaluated = getRoot()->substituteActionExpression(getRoot()->paths[path], action);
-            action_path_expression[action].push_back(evaluated);
-        }
-    }
 
-    std::vector<std::vector<uint64_t>> state_dont_care_actions(numStates());
-    for(uint64_t state: state_is_relevant) {
-        state_dont_care_actions[state].push_back(dont_care_action);
-        for(uint64_t action: ~state_available_actions[state]) {
-            state_dont_care_actions[state].push_back(action);
+        for(uint64_t value: state_valuation[state]) {
+            state_valuation_int.push_back(ctx.int_val(value));
         }
-    }
-
+        timers["ColoringSmt::1-2 createPrefixSubstitutions"].start();
+        getRoot()->createPrefixSubstitutions(state_valuation[state], state_valuation_int);
+        timers["ColoringSmt::1-2 createPrefixSubstitutions"].stop();
+        state_valuation_int.resize(0);
 
-    for(uint64_t state = 0; state < numStates(); ++state) {
-        for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) {
-            choice_path_expresssion.push_back(z3::expr_vector(ctx));
-            if(not state_is_relevant[state]) {
-                continue;
-            }
-            uint64_t action = choice_to_action[choice];
-            for(uint64_t path = 0; path < numPaths(); ++path) {
-                z3::expr action_selection = action_path_expression[action][path];
+        timers["ColoringSmt::1-3"].start();
+        for(uint64_t path = 0; path < numPaths(); ++path) {
+            timers["ColoringSmt::1-3-1"].start();
+            getRoot()->substitutePrefixExpression(getRoot()->paths[path], clause_array);
+            timers["ColoringSmt::1-3-1"].stop();
+
+            timers["ColoringSmt::1-3-2"].start();
+            for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) {
+                timers["ColoringSmt::1-3-2-1"].start();
+                uint64_t num_clauses = getRoot()->paths[path].size()-1;
+                uint64_t action = choice_to_action[choice];
+                clause_array[num_clauses++] = terminals[path]->action_expression[action];
+                timers["ColoringSmt::1-3-2-1"].stop();
+                timers["ColoringSmt::1-3-2-2"].start();
                 if(action == dont_care_action) {
-                    action_selection = getRoot()->substituteActionExpression(getRoot()->paths[path], state_dont_care_actions[state]);
+                    for(uint64_t unavailable_action: ~state_available_actions[state]) {
+                        clause_array[num_clauses++] = terminals[path]->action_expression[unavailable_action];
+                    }
                 }
-                choice_path_expresssion[choice].push_back(state_path_expression[state][path] or action_selection);
+                timers["ColoringSmt::1-3-2-2"].stop();
+                choice_path_expresssion[choice].push_back(z3::expr(ctx, Z3_mk_or(ctx, num_clauses, clause_array.ptr())));
+                // choice_path_expresssion[choice].push_back(Z3_mk_or(ctx, num_clauses, clause_array.ptr()));
             }
+            timers["ColoringSmt::1-3-2"].stop();
         }
+        timers["ColoringSmt::1-3"].stop();
     }
-    timers["ColoringSmt:: create choice colors"].stop();
+    timers["ColoringSmt::1 create choice colors"].stop();
 
     if(not this->enable_harmonization) {
         timers[__FUNCTION__].stop();
         return;
     }
 
-    timers["ColoringSmt:: create harmonizing variants"].start();
-
+    timers["ColoringSmt::2 create harmonizing variants"].start();
+    // std::cout << "ColoringSmt::2 create harmonizing variants" << std::endl << std::flush;
 
-    // create harmonizing expressions
-    std::vector<z3::expr_vector> state_path_expression_harmonizing;
+    getRoot()->substituteActionExpressionsHarmonizing(harmonizing_variable);
+    choice_path_expresssion_harm.resize(numChoices());
     for(uint64_t state = 0; state < numStates(); ++state) {
-        state_path_expression_harmonizing.push_back(z3::expr_vector(ctx));
         if(not state_is_relevant[state]) {
             continue;
         }
-        // create state substitution
-        z3::expr_vector substitution_expr(ctx);
+
         for(uint64_t value: state_valuation[state]) {
-            substitution_expr.push_back(ctx.int_val(value));
-        }
-        getRoot()->createPrefixSubstitutionsHarmonizing(substitution_expr);
-        for(uint64_t path = 0; path < numPaths(); ++path) {
-            z3::expr_vector evaluated(ctx);
-            getRoot()->substitutePrefixExpressionHarmonizing(getRoot()->paths[path], evaluated);
-            state_path_expression_harmonizing[state].push_back(z3::mk_or(evaluated));
+            state_valuation_int.push_back(ctx.int_val(value));
         }
-    }
-    std::vector<z3::expr_vector> action_path_expression_harmonizing;
-    for(uint64_t action = 0; action < num_actions; ++action) {
-        action_path_expression_harmonizing.push_back(z3::expr_vector(ctx));
+        timers["ColoringSmt::2-2 createPrefixSubstitutionsHarmonizing"].start();
+        getRoot()->createPrefixSubstitutionsHarmonizing(state_valuation[state], state_valuation_int, harmonizing_variable);
+        timers["ColoringSmt::2-2 createPrefixSubstitutionsHarmonizing"].stop();
+        state_valuation_int.resize(0);
+
+        timers["ColoringSmt::2-3"].start();
         for(uint64_t path = 0; path < numPaths(); ++path) {
-            z3::expr evaluated = getRoot()->substituteActionExpressionHarmonizing(getRoot()->paths[path], action, harmonizing_variable);
-            action_path_expression_harmonizing[action].push_back(evaluated);
-        }
-    }
-    for(uint64_t state = 0; state < numStates(); ++state) {
-        for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) {
-            choice_path_expresssion_harm.push_back(z3::expr_vector(ctx));
-            if(not state_is_relevant[state]) {
-                continue;
-            }
-            uint64_t action = choice_to_action[choice];
-            for(uint64_t path = 0; path < numPaths(); ++path) {
-                z3::expr action_selection = action_path_expression_harmonizing[action][path];
+            timers["ColoringSmt::2-3-1"].start();
+            getRoot()->substitutePrefixExpressionHarmonizing(getRoot()->paths[path], clause_array);
+            timers["ColoringSmt::2-3-1"].stop();
+
+            timers["ColoringSmt::2-3-2"].start();
+            for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) {
+                uint64_t action = choice_to_action[choice];
+                uint64_t num_clauses = getRoot()->paths[path].size()-1;
+                clause_array[num_clauses++] = terminals[path]->action_expression_harmonizing[action];
                 if(action == dont_care_action) {
-                    action_selection = getRoot()->substituteActionExpressionHarmonizing(getRoot()->paths[path], state_dont_care_actions[state], harmonizing_variable);
+                    for(uint64_t unavailable_action: ~state_available_actions[state]) {
+                        clause_array[num_clauses++] = terminals[path]->action_expression_harmonizing[unavailable_action];
+                    }
                 }
-                choice_path_expresssion_harm[choice].push_back(state_path_expression_harmonizing[state][path] or action_selection);
+                choice_path_expresssion_harm[choice].push_back(z3::expr(ctx, Z3_mk_or(ctx, num_clauses, clause_array.ptr())));
+                // choice_path_expresssion_harm[choice].push_back(Z3_mk_or(ctx, num_clauses, clause_array.ptr()));
             }
+            timers["ColoringSmt::2-3-2"].stop();
         }
+        timers["ColoringSmt::2-3"].stop();
     }
-    timers["ColoringSmt:: create harmonizing variants"].stop();
+    timers["ColoringSmt::2 create harmonizing variants"].stop();
+
+    getRoot()->clearCache();
 
     timers[__FUNCTION__].stop();
 }
 
+template<typename ValueType>
+ColoringSmt<ValueType>::~ColoringSmt() {
+    tree.clear();
+}
+
 template<typename ValueType>
 void ColoringSmt<ValueType>::enableStateExploration(storm::models::sparse::NondeterministicModel<ValueType> const& model) {
     this->state_exploration_enabled = true;
@@ -530,7 +530,6 @@ std::pair<bool,std::vector<std::vector<uint64_t>>> ColoringSmt<ValueType>::areCh
         }
     }*/
 
-
     timers["areChoicesConsistent::1 is scheduler consistent?"].start();
     solver.push();
     getRoot()->addFamilyEncoding(subfamily,solver);
@@ -543,6 +542,7 @@ std::pair<bool,std::vector<std::vector<uint64_t>>> ColoringSmt<ValueType>::areCh
         for(uint64_t path: state_path_enabled[state]) {
             const char *label = choice_path_label[choice][path].c_str();
             solver.add(choice_path_expresssion[choice][path], label);
+            // Z3_solver_assert_and_track(ctx, solver.operator Z3_solver(), choice_path_expresssion[choice][path], ctx.bool_const(label));
         }
     }
     bool consistent = check();
@@ -584,6 +584,7 @@ std::pair<bool,std::vector<std::vector<uint64_t>>> ColoringSmt<ValueType>::areCh
                 for(uint64_t path: state_path_enabled[state]) {
                     const char *label = choice_path_label[choice][path].c_str();
                     solver.add(choice_path_expresssion[choice][path], label);
+                    // Z3_solver_assert_and_track(ctx, solver.operator Z3_solver(), choice_path_expresssion[choice][path], ctx.bool_const(label));
                 }
                 consistent = check();
             }
@@ -603,6 +604,7 @@ std::pair<bool,std::vector<std::vector<uint64_t>>> ColoringSmt<ValueType>::areCh
     for(auto [choice,path]: this->unsat_core) {
         const char *label = choice_path_label[choice][path].c_str();
         solver.add(choice_path_expresssion_harm[choice][path], label);
+        // Z3_solver_assert_and_track(ctx, solver.operator Z3_solver(), choice_path_expresssion_harm[choice][path], ctx.bool_const(label));
     }
 
     z3::model model(ctx);

payntbind/src/synthesis/quotient/ColoringSmt.h

@@ -48,6 +48,8 @@ class ColoringSmt {
         bool enable_harmonization
     );
 
+    ~ColoringSmt();
+
     /**
      * Enable efficient state exploration of reachable states.
      * @note this is required for harmonization
@@ -156,14 +158,17 @@ class ColoringSmt {
     /** For each choice and path, a label passed to SMT solver. */
     std::vector<std::vector<std::string>> choice_path_label;
     /** For each choice, its color expressed as a conjunction of all path implications. */
-    std::vector<z3::expr_vector> choice_path_expresssion;
+    std::vector<std::vector<z3::expr>> choice_path_expresssion;
+    // std::vector<std::vector<Z3_ast>> choice_path_expresssion;
+
 
     /** Whether harmonization is required. */
     const bool enable_harmonization;
     /** SMT variable refering to harmonizing hole. */
     z3::expr harmonizing_variable;
     /** For each choice, its color expressed as a conjunction of all path implications. */
-    std::vector<z3::expr_vector> choice_path_expresssion_harm;
+    std::vector<std::vector<z3::expr>> choice_path_expresssion_harm;
+    // std::vector<std::vector<Z3_ast>> choice_path_expresssion_harm;
 
     /** For each state, whether (in the last subfamily) the path was enabled. */
     std::vector<BitVector> state_path_enabled;