diff --git a/paynt/synthesizer/decision_tree.py b/paynt/synthesizer/decision_tree.py index 80c87f75..ccd6932d 100644 --- a/paynt/synthesizer/decision_tree.py +++ b/paynt/synthesizer/decision_tree.py @@ -59,7 +59,6 @@ def harmonize_inconsistent_scheduler(self, family): def verify_family(self, family): self.num_families_considered += 1 - self.quotient.build(family) if family.mdp is None: self.num_families_skipped += 1 @@ -85,6 +84,7 @@ def verify_family(self, family): return self.harmonize_inconsistent_scheduler(family) + def counters_reset(self): self.num_families_considered = 0 self.num_families_skipped = 0 @@ -110,6 +110,10 @@ def synthesize_tree(self, depth:int): def synthesize_tree_sequence(self, opt_result_value): tree_hint = None + global_timeout = paynt.utils.timer.GlobalTimer.global_timer.time_limit_seconds + if global_timeout is None: + global_timeout = 300 + depth_timeout = global_timeout / 2 / SynthesizerDecisionTree.tree_depth for depth in range(SynthesizerDecisionTree.tree_depth+1): print() self.quotient.set_depth(depth) @@ -120,7 +124,8 @@ def synthesize_tree_sequence(self, opt_result_value): self.counters_reset() self.stat = paynt.synthesizer.statistic.Statistic(self) self.stat.start(family) - self.synthesis_timer = paynt.utils.timer.Timer() + timeout = depth_timeout if depth < SynthesizerDecisionTree.tree_depth else None + self.synthesis_timer = paynt.utils.timer.Timer(timeout) self.synthesis_timer.start() families = [family] @@ -133,6 +138,7 @@ def synthesize_tree_sequence(self, opt_result_value): self.synthesize_one(family) self.stat.finished_synthesis() self.stat.print() + self.synthesis_timer = None self.counters_print() new_assignment_synthesized = self.best_assignment != best_assignment_old diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index 7de35bb3..8916adde 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -50,9 +50,20 @@ ColoringSmt::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(); - uint64_t num_actions = *std::max_element(choice_to_action.begin(),choice_to_action.end())-1; + uint64_t num_actions = *std::max_element(choice_to_action.begin(),choice_to_action.end())+1; for(uint64_t node = 0; node < num_nodes; ++node) { auto [parent,child_true,child_false] = tree_list[node]; STORM_LOG_THROW( @@ -60,23 +71,17 @@ ColoringSmt::ColoringSmt( "Inner node has only one child." ); if(child_true != num_nodes) { - tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain)); + tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,state_substitution_variables)); } else { - tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,num_actions)); + tree.push_back(std::make_shared(node,ctx,this->variable_name,this->variable_domain,num_actions,action_substitution_variable)); } } getRoot()->createTree(tree_list,tree); - // create substitution variables - z3::expr_vector substitution_variables(ctx); - for(auto const& name: variable_name) { - substitution_variables.push_back(ctx.int_const(name.c_str())); - } - substitution_variables.push_back(ctx.int_const("act")); getRoot()->createHoles(family); - getRoot()->createPaths(substitution_variables); harmonizing_variable = ctx.int_const("__harm__"); - getRoot()->createPathsHarmonizing(substitution_variables, harmonizing_variable); + getRoot()->createPaths(harmonizing_variable); + for(uint64_t state = 0; state < numStates(); ++state) { state_path_enabled.push_back(BitVector(numPaths())); } @@ -105,6 +110,17 @@ ColoringSmt::ColoringSmt( } // create choice substitutions + std::vector state_substitution_expr; + for(uint64_t state = 0; state < numStates(); ++state) { + z3::expr_vector substitution_expr(ctx); + for(uint64_t value: state_valuation[state]) { + substitution_expr.push_back(ctx.int_val(value)); + } + state_substitution_expr.push_back(substitution_expr); + } + + // create choice substitutions + // std::vector choice_action_substitution_expr; std::vector choice_substitution_expr; for(uint64_t state = 0; state < numStates(); ++state) { for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { @@ -112,7 +128,8 @@ ColoringSmt::ColoringSmt( for(uint64_t value: state_valuation[state]) { substitution_expr.push_back(ctx.int_val(value)); } - substitution_expr.push_back(ctx.int_val(choice_to_action[choice])); + z3::expr action_substitution_expr = ctx.int_val(choice_to_action[choice]); + substitution_expr.push_back(action_substitution_expr); choice_substitution_expr.push_back(substitution_expr); } } @@ -132,17 +149,41 @@ ColoringSmt::ColoringSmt( // create choice colors timers["ColoringSmt:: create choice colors"].start(); + + choice_path_label.resize(numChoices()); for(uint64_t state = 0; state < numStates(); ++state) { for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { - std::vector path_label; - z3::expr_vector path_evaluated(ctx); for(uint64_t path = 0; path < numPaths(); ++path) { std::string label = "p" + std::to_string(choice) + "_" + std::to_string(path); - path_label.push_back(label); - path_evaluated.push_back(path_expression[path].substitute(substitution_variables,choice_substitution_expr[choice])); - // path_evaluated.push_back(path_expression[path].substitute(substitution_variables,choice_substitution_expr[choice]).simplify()); + choice_path_label[choice].push_back(label); + } + } + } + + /*std::vector state_path_expresssion; + for(uint64_t state = 0; state < numStates(); ++state) { + z3::expr_vector path_evaluated(ctx); + for(uint64_t path = 0; path < numPaths(); ++path) { + path_evaluated.push_back(path_expression[path].substitute(state_substitution_variables,state_substitution_expr[state])); + } + state_path_expresssion.push_back(path_evaluated); + } + + for(uint64_t state = 0; state < numStates(); ++state) { + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + z3::expr_vector path_evaluated(ctx); + for(uint64_t path = 0; path < numPaths(); ++path) { + path_evaluated.push_back(state_path_expresssion[state][path].substitute(action_substitution_variables,choice_action_substitution_expr[choice])); + } + choice_path_expresssion.push_back(path_evaluated); + } + }*/ + for(uint64_t state = 0; state < numStates(); ++state) { + for(uint64_t choice = row_groups[state]; choice < row_groups[state+1]; ++choice) { + z3::expr_vector path_evaluated(ctx); + for(uint64_t path = 0; path < numPaths(); ++path) { + path_evaluated.push_back(path_expression[path].substitute(choice_substitution_variables,choice_substitution_expr[choice])); } - choice_path_label.push_back(path_label); choice_path_expresssion.push_back(path_evaluated); } } @@ -153,47 +194,34 @@ ColoringSmt::ColoringSmt( return; } - timers["ColoringSmt:: create harmonizing variants (1)"].start(); - // create harmonizing variants - std::vector all_holes(family.numHoles()); - getRoot()->loadAllHoles(all_holes); - std::vector hole_what; - std::vector hole_with; - for(const TreeNode::Hole *hole: all_holes) { - z3::expr_vector what(ctx); what.push_back(hole->solver_variable); hole_what.push_back(what); - z3::expr_vector with(ctx); with.push_back(hole->solver_variable_harm); hole_with.push_back(with); - } - - std::vector>> path_step_holes(numPaths()); - for(uint64_t path = 0; path < numPaths(); ++path) { - getRoot()->loadPathStepHoles(getRoot()->paths[path],path_step_holes[path]); - } - - z3::expr_vector path_expression_harmonizing(ctx); - for(uint64_t path = 0; path < numPaths(); ++path) { - z3::expr_vector variants(ctx); - variants.push_back(path_expression[path]); - for(uint64_t step = 0; step < path_step_expression[path].size(); ++step) { - for(uint64_t hole: path_step_holes[path][step]) { - variants.push_back( - (harmonizing_variable == (int)hole) and path_step_expression[path][step].substitute(hole_what[hole],hole_with[hole]) - ); - } + timers["ColoringSmt:: create harmonizing variants"].start(); + std::vector state_path_expression_harmonizing; + for(uint64_t state = 0; state < numStates(); ++state) { + state_path_expression_harmonizing.push_back(z3::expr_vector(ctx)); + for(uint64_t path = 0; path < numPaths(); ++path) { + z3::expr_vector evaluated(ctx); + getRoot()->substitutePrefixExpressionHarmonizing(getRoot()->paths[path], state_substitution_expr[state], evaluated); + state_path_expression_harmonizing[state].push_back(z3::mk_or(evaluated)); } - path_expression_harmonizing.push_back(z3::mk_or(variants)); } - timers["ColoringSmt:: create harmonizing variants (1)"].stop(); - - for(uint64_t choice = 0; choice < numChoices(); ++choice) { - choice_path_expresssion_harm.push_back(z3::expr_vector(ctx)); + std::vector action_path_expression_harmonizing; + for(uint64_t action = 0; action < num_actions; ++action) { + action_path_expression_harmonizing.push_back(z3::expr_vector(ctx)); + 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); + } } - timers["ColoringSmt:: create harmonizing variants (2)"].start(); - for(uint64_t path = 0; path < numPaths(); ++path) { - for(uint64_t choice = 0; choice < numChoices(); ++choice) { - choice_path_expresssion_harm[choice].push_back(path_expression_harmonizing[path].substitute(substitution_variables,choice_substitution_expr[choice])); + 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)); + uint64_t action = choice_to_action[choice]; + for(uint64_t path = 0; path < numPaths(); ++path) { + choice_path_expresssion_harm[choice].push_back(state_path_expression_harmonizing[state][path] or action_path_expression_harmonizing[action][path]); + } } } - timers["ColoringSmt:: create harmonizing variants (2)"].stop(); + timers["ColoringSmt:: create harmonizing variants"].stop(); timers[__FUNCTION__].stop(); } @@ -428,6 +456,7 @@ std::pair>> ColoringSmt::areCh solver.add(choice_path_expresssion[choice][path], label); } } + // std::cout << "(1) added choices: " << choices.getNumberOfSetBits() << std::endl; bool consistent = check(); timers["areChoicesConsistent::1 is scheduler consistent?"].stop(); @@ -448,6 +477,7 @@ std::pair>> ColoringSmt::areCh BitVector state_reached(numStates(),false); state_reached.set(initial_state,true); consistent = true; + uint64_t num_choices_added = 0; while(consistent) { STORM_LOG_THROW(not unexplored_states.empty(), storm::exceptions::UnexpectedException, "all states explored but UNSAT core not found"); uint64_t state = unexplored_states.front(); unexplored_states.pop(); @@ -459,6 +489,7 @@ std::pair>> ColoringSmt::areCh const char *label = choice_path_label[choice][path].c_str(); solver.add(choice_path_expresssion[choice][path], label); } + // std::cout << "(2) adding choice " << (++num_choices_added) << std::endl; consistent = check(); if(not consistent) { break; diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp index db3611c6..f3956afb 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.cpp +++ b/payntbind/src/synthesis/quotient/TreeNode.cpp @@ -135,10 +135,13 @@ const TreeNode *TreeNode::getNodeOfPath(std::vector const& path, uint64_t TerminalNode::TerminalNode( uint64_t identifier, z3::context & ctx, - std::vector const& variable_name, std::vector> const& variable_domain, - uint64_t num_actions -) : TreeNode(identifier,ctx,variable_name,variable_domain), num_actions(num_actions), action_hole(false,ctx), - action_expr(ctx), action_expr_harm(ctx) {} + std::vector const& variable_name, + std::vector> const& variable_domain, + uint64_t num_actions, + z3::expr const& action_substitution_variable +) : TreeNode(identifier,ctx,variable_name,variable_domain), + num_actions(num_actions), action_substitution_variable(action_substitution_variable), + action_hole(false,ctx), action_expr(ctx), action_expr_harm(ctx) {} void TerminalNode::createHoles(Family& family) { action_hole.hole = family.addHole(num_actions); @@ -151,22 +154,28 @@ void TerminalNode::loadHoleInfo(std::vector const& path, z3::expr_vector & expression) const { expression.push_back(action_expr); } +void TerminalNode::loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const { + expression.push_back(action_expr_harm); +} + +void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { + // +} + +z3::expr TerminalNode::substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const { + return action_hole.solver_variable == (int)action or (harmonizing_variable == (int)action_hole.hole and action_hole.solver_variable_harm == (int)action); +} + void TerminalNode::loadAllHoles(std::vector & holes) const { holes[action_hole.hole] = &action_hole; } @@ -217,8 +226,10 @@ void TerminalNode::unsatCoreAnalysis( InnerNode::InnerNode( uint64_t identifier, z3::context & ctx, std::vector const& variable_name, - std::vector> const& variable_domain -) : TreeNode(identifier,ctx,variable_name,variable_domain), decision_hole(false,ctx), + std::vector> const& variable_domain, + z3::expr_vector const& state_substitution_variables +) : TreeNode(identifier,ctx,variable_name,variable_domain), + decision_hole(false,ctx), state_substitution_variables(state_substitution_variables), step_true(ctx), step_false(ctx), step_true_harm(ctx), step_false_harm(ctx) {} void InnerNode::createHoles(Family& family) { @@ -276,23 +287,10 @@ void InnerNode::loadHoleInfo(std::vectorloadHoleInfo(hole_info); } -void InnerNode::createPaths(z3::expr_vector const& substitution_variables) { - child_true->createPaths(substitution_variables); - child_false->createPaths(substitution_variables); +void InnerNode::createPaths(z3::expr const& harmonizing_variable) { - // create steps - z3::expr_vector step_true_options(ctx); - z3::expr_vector step_false_options(ctx); - for(uint64_t variable = 0; variable < numVariables(); ++variable) { - z3::expr const& dv = decision_hole.solver_variable; - z3::expr const& vv = variable_hole[variable].solver_variable; - - step_true_options.push_back( dv == (int)variable and substitution_variables[variable] <= vv); - step_false_options.push_back(dv == (int)variable and substitution_variables[variable] > vv); - } - // mind the negation below - step_true = not z3::mk_or(step_true_options); - step_false = not z3::mk_or(step_false_options); + child_true->createPaths(harmonizing_variable); + child_false->createPaths(harmonizing_variable); // create paths for(bool condition: {true,false}) { @@ -304,33 +302,74 @@ void InnerNode::createPaths(z3::expr_vector const& substitution_variables) { paths.push_back(path); } } -} - -void InnerNode::createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) { - child_true->createPathsHarmonizing(substitution_variables, harmonizing_variable); - child_false->createPathsHarmonizing(substitution_variables, harmonizing_variable); // create steps z3::expr_vector step_true_options(ctx); z3::expr_vector step_false_options(ctx); - z3::expr const& hv = harmonizing_variable; for(uint64_t variable = 0; variable < numVariables(); ++variable) { - Hole d = decision_hole; - z3::expr de = d.solver_variable == (int)variable; - z3::expr deh = d.solver_variable_harm == (int)variable; - z3::expr expr_decision = (hv != (int)d.hole and de) or (hv == (int)d.hole and ((not de and deh) or (de and not deh)) ); - - Hole v = variable_hole[variable]; - z3::expr ve = substitution_variables[variable] <= v.solver_variable; - z3::expr veh = substitution_variables[variable] <= v.solver_variable_harm; - z3::expr expr_true = (hv != (int)v.hole and ve) or (hv == (int)v.hole and ((not ve and veh) or (ve and not veh)) ); - z3::expr expr_false = (hv != (int)v.hole and not ve) or (hv == (int)v.hole and ((ve and not veh) or (not ve and veh)) ); - - step_true_options.push_back(expr_decision and expr_true); - step_false_options.push_back(expr_decision and expr_false); + z3::expr const& dv = decision_hole.solver_variable; + z3::expr const& vv = variable_hole[variable].solver_variable; + // mind the negation below + step_true_options.push_back( not(dv == (int)variable and state_substitution_variables[variable] <= vv)); + step_false_options.push_back(not(dv == (int)variable and state_substitution_variables[variable] > vv)); } - step_true_harm = z3::mk_or(step_true_options); - step_false_harm = z3::mk_or(step_false_options); + step_true = z3::mk_and(step_true_options); + step_false = z3::mk_and(step_false_options); + + // create steps (harmonizing) + z3::expr_vector step_true_harm_options(ctx); + z3::expr_vector step_false_harm_options(ctx); + + z3::expr_vector what(ctx); what.push_back(decision_hole.solver_variable); + z3::expr_vector with(ctx); with.push_back(decision_hole.solver_variable_harm); + z3::expr dtrue = harmonizing_variable == (int)decision_hole.hole and step_true.substitute(what,with); + z3::expr dfalse = harmonizing_variable == (int)decision_hole.hole and step_false.substitute(what,with); + + for(uint64_t var = 0; var < numVariables(); ++var) { + Hole const& hole = variable_hole[var]; + z3::expr const& dv = decision_hole.solver_variable; + z3::expr const& vv = variable_hole[var].solver_variable; + z3::expr const& vvh = variable_hole[var].solver_variable_harm; + step_true_harm_options.push_back( not(dv == (int)var and state_substitution_variables[var] <= vv) or (harmonizing_variable == (int)hole.hole and not(state_substitution_variables[var] <= vvh) ) ); + step_false_harm_options.push_back( not(dv == (int)var and state_substitution_variables[var] > vv) or (harmonizing_variable == (int)hole.hole and not(state_substitution_variables[var] > vvh) ) ); + } + + step_true_harm = dtrue or z3::mk_and(step_true_harm_options); + step_false_harm = dfalse or z3::mk_and(step_false_harm_options); + + /*step_true_harm_options.push_back(step_true); + step_false_harm_options.push_back(step_false); + + z3::expr_vector what(ctx); what.push_back(decision_hole.solver_variable); + z3::expr_vector with(ctx); with.push_back(decision_hole.solver_variable_harm); + step_true_harm_options.push_back(harmonizing_variable == (int)decision_hole.hole and step_true.substitute(what,with)); + step_false_harm_options.push_back(harmonizing_variable == (int)decision_hole.hole and step_false.substitute(what,with)); + for(uint64_t variable = 0; variable < numVariables(); ++variable) { + Hole const& hole = variable_hole[variable]; + + // create steps + z3::expr_vector step_true_options(ctx); + z3::expr_vector step_false_options(ctx); + step_true_options.push_back(harmonizing_variable == (int)hole.hole); + step_false_options.push_back(harmonizing_variable == (int)hole.hole); + for(uint64_t var = 0; var < numVariables(); ++var) { + z3::expr const& dv = decision_hole.solver_variable; + z3::expr const& vv = variable_hole[var].solver_variable; + z3::expr const& vvh = variable_hole[var].solver_variable_harm; + // mind the negation below + if(var != variable) { + step_true_options.push_back( not(dv == (int)var and substitution_variables[var] <= vv)); + step_false_options.push_back(not(dv == (int)var and substitution_variables[var] > vv)); + } else { + step_true_options.push_back( not(substitution_variables[var] <= vvh)); + step_false_options.push_back(not(substitution_variables[var] > vvh)); + } + } + step_true_harm_options.push_back(z3::mk_and(step_true_options)); + step_false_harm_options.push_back(z3::mk_and(step_false_options)); + } + step_true_harm = z3::mk_or(step_true_harm_options); + step_false_harm = z3::mk_or(step_false_harm_options);*/ } void InnerNode::loadPathExpression(std::vector const& path, z3::expr_vector & expression) const { @@ -340,6 +379,26 @@ void InnerNode::loadPathExpression(std::vector const& path, z3::expr_vecto getChild(step_to_true_child)->loadPathExpression(path,expression); } +void InnerNode::loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const { + bool step_to_true_child = path[depth]; + z3::expr const& step = step_to_true_child ? step_true_harm : step_false_harm; + expression.push_back(step); + getChild(step_to_true_child)->loadPathExpressionHarmonizing(path,expression); +} + +void InnerNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { + bool step_to_true_child = path[depth]; + z3::expr step = step_to_true_child ? step_true_harm : step_false_harm; + substituted.push_back(step.substitute(state_substitution_variables,state_valuation)); + getChild(step_to_true_child)->substitutePrefixExpressionHarmonizing(path,state_valuation,substituted); +} + +z3::expr InnerNode::substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const { + return getChild(path[depth])->substituteActionExpressionHarmonizing(path,action,harmonizing_variable); +} + + + void InnerNode::loadAllHoles(std::vector & holes) const { holes[decision_hole.hole] = &decision_hole; for(Hole const& hole: variable_hole) { diff --git a/payntbind/src/synthesis/quotient/TreeNode.h b/payntbind/src/synthesis/quotient/TreeNode.h index 4937ec02..6097a473 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.h +++ b/payntbind/src/synthesis/quotient/TreeNode.h @@ -113,12 +113,16 @@ class TreeNode { virtual void loadHoleInfo(std::vector> & hole_info) const {} /** Create a list of paths from this node. */ - virtual void createPaths(z3::expr_vector const& substitution_variables) {} - /** Create a list of paths from this node. */ - virtual void createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) {} + virtual void createPaths(z3::expr const& harmonizing_variable) {} + /** Create expression for a path. */ virtual void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const {} + /** Create expression for a harmonizing path. */ + virtual void loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const {} /** TODO */ + virtual void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {} + virtual z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const { return z3::expr(ctx); } + virtual void loadAllHoles(std::vector & holes) const {}; virtual void loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const {}; @@ -153,6 +157,7 @@ class TreeNode { class TerminalNode: public TreeNode { public: const uint64_t num_actions; + z3::expr action_substitution_variable; Hole action_hole; z3::expr action_expr; z3::expr action_expr_harm; @@ -161,14 +166,19 @@ class TerminalNode: public TreeNode { uint64_t identifier, z3::context & ctx, std::vector const& variable_name, std::vector> const& variable_domain, - uint64_t num_actions + uint64_t num_actions, + z3::expr const& action_substitution_variable ); void createHoles(Family& family) override; void loadHoleInfo(std::vector> & hole_info) const override; - void createPaths(z3::expr_vector const& substitution_variables) override; - void createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) override; + void createPaths(z3::expr const& harmonizing_variable) override; + void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const override; + void loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const override; + void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; + z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const override; + void loadAllHoles(std::vector & holes) const override; void loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const override; @@ -201,6 +211,7 @@ class InnerNode: public TreeNode { Hole decision_hole; std::vector variable_hole; + z3::expr_vector state_substitution_variables; z3::expr step_true; z3::expr step_false; @@ -211,14 +222,19 @@ class InnerNode: public TreeNode { InnerNode( uint64_t identifier, z3::context & ctx, std::vector const& variable_name, - std::vector> const& variable_domain + std::vector> const& variable_domain, + z3::expr_vector const& state_substitution_variables ); void createHoles(Family& family) override; void loadHoleInfo(std::vector> & hole_info) const override; - void createPaths(z3::expr_vector const& substitution_variables) override; - void createPathsHarmonizing(z3::expr_vector const& substitution_variables, z3::expr const& harmonizing_variable) override; + void createPaths(z3::expr const& harmonizing_variable) override; + void loadPathExpression(std::vector const& path, z3::expr_vector & expression) const override; + void loadPathExpressionHarmonizing(std::vector const& path, z3::expr_vector & expression) const override; + void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; + z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const override; + void loadAllHoles(std::vector & holes) const override; void loadPathStepHoles(std::vector const& path, std::vector> & step_holes) const override;