From efcc20277317412d1299b023c590c83ca26c6d53 Mon Sep 17 00:00:00 2001 From: Roman Andriushchenko Date: Fri, 4 Oct 2024 00:16:55 +0200 Subject: [PATCH] faster path formula creation --- .../src/synthesis/quotient/ColoringSmt.cpp | 15 +++-- .../src/synthesis/quotient/ColoringSmt.h | 6 +- payntbind/src/synthesis/quotient/TreeNode.cpp | 65 +++++++++++++------ payntbind/src/synthesis/quotient/TreeNode.h | 24 +++++-- 4 files changed, 73 insertions(+), 37 deletions(-) diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.cpp b/payntbind/src/synthesis/quotient/ColoringSmt.cpp index d64d9ec1..3c9723a7 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.cpp +++ b/payntbind/src/synthesis/quotient/ColoringSmt.cpp @@ -137,20 +137,20 @@ ColoringSmt::ColoringSmt( std::vector state_path_expression; for(uint64_t state = 0; state < numStates(); ++state) { + getRoot()->createPrefixSubstitutions(state_valuation[state]); state_path_expression.push_back(z3::expr_vector(ctx)); for(uint64_t path = 0; path < numPaths(); ++path) { - z3::expr_vector substituted(ctx); - // getRoot()->substitutePrefixExpression(getRoot()->paths[path], state_substitution_expr[state], substituted); - getRoot()->substitutePrefixExpression(getRoot()->paths[path], state_valuation[state], substituted); - state_path_expression[state].push_back(z3::mk_or(substituted)); + z3::expr_vector evaluated(ctx); + getRoot()->substitutePrefixExpression(getRoot()->paths[path], evaluated); + state_path_expression[state].push_back(z3::mk_or(evaluated)); } } std::vector action_path_expression; for(uint64_t action = 0; action < num_actions; ++action) { action_path_expression.push_back(z3::expr_vector(ctx)); for(uint64_t path = 0; path < numPaths(); ++path) { - z3::expr substituted = getRoot()->substituteActionExpression(getRoot()->paths[path], action); - action_path_expression[action].push_back(substituted); + z3::expr evaluated = getRoot()->substituteActionExpression(getRoot()->paths[path], action); + action_path_expression[action].push_back(evaluated); } } @@ -173,10 +173,11 @@ ColoringSmt::ColoringSmt( timers["ColoringSmt:: create harmonizing variants"].start(); std::vector state_path_expression_harmonizing; for(uint64_t state = 0; state < numStates(); ++state) { + getRoot()->createPrefixSubstitutionsHarmonizing(state_substitution_expr[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); + getRoot()->substitutePrefixExpressionHarmonizing(getRoot()->paths[path], evaluated); state_path_expression_harmonizing[state].push_back(z3::mk_or(evaluated)); } } diff --git a/payntbind/src/synthesis/quotient/ColoringSmt.h b/payntbind/src/synthesis/quotient/ColoringSmt.h index 88653b94..d1a38237 100644 --- a/payntbind/src/synthesis/quotient/ColoringSmt.h +++ b/payntbind/src/synthesis/quotient/ColoringSmt.h @@ -65,6 +65,9 @@ class ColoringSmt { protected: + /** If true, the object will be setup for one consistency check. */ + bool disable_counterexamples; + /** The initial state. */ const uint64_t initial_state; /** Valuation of each state. */ @@ -133,9 +136,6 @@ class ColoringSmt { bool PRINT_UNSAT_CORE = false; void loadUnsatCore(z3::expr_vector const& unsat_core_expr, Family const& subfamily); - /** If true, the object will be setup for one consistency check. */ - bool disable_counterexamples; - }; } \ No newline at end of file diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp index ea68af24..2f3c722b 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.cpp +++ b/payntbind/src/synthesis/quotient/TreeNode.cpp @@ -164,8 +164,11 @@ uint64_t TerminalNode::getPathActionHole(std::vector const& path) { return action_hole.hole; } +void TerminalNode::createPrefixSubstitutions(std::vector const& state_valuation) { + // +} -void TerminalNode::substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const { +void TerminalNode::substitutePrefixExpression(std::vector const& path, z3::expr_vector & substituted) const { // } @@ -173,7 +176,11 @@ z3::expr TerminalNode::substituteActionExpression(std::vector const& path, return action_hole.solver_variable == (int)action; } -void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { +void TerminalNode::createPrefixSubstitutionsHarmonizing(z3::expr_vector const& state_valuation) { + // +} + +void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector & substituted) const { // } @@ -227,7 +234,7 @@ InnerNode::InnerNode( 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) {} + step_true(ctx), step_false(ctx), substituted_true(ctx), substituted_false(ctx), step_true_harm(ctx), step_false_harm(ctx) {} void InnerNode::createHoles(Family& family) { decision_hole.hole = family.addHole(numVariables()); @@ -374,43 +381,59 @@ uint64_t InnerNode::getPathActionHole(std::vector const& path) { } -void InnerNode::substitutePrefixExpression(std::vector const& path, std::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 : step_false; - // substituted.push_back(step.substitute(state_substitution_variables,state_valuation)); - - z3::expr_vector step_options(ctx); +void InnerNode::createPrefixSubstitutions(std::vector const& state_valuation) { + z3::expr_vector step_options_true(ctx); + z3::expr_vector step_options_false(ctx); z3::expr const& dv = decision_hole.solver_variable; for(uint64_t variable = 0; variable < numVariables(); ++variable) { z3::expr const& vv = variable_hole[variable].solver_variable; // mind the negation below - if(step_to_true_child) { - if(state_valuation[variable] > 0) { - // not (Vi = vj => sj<=xj) - step_options.push_back( dv == ctx.int_val(variable) and not(ctx.int_val(state_valuation[variable]) <= vv)); - } - } else { - if(state_valuation[variable] < variable_domain[variable].size()-1) { - step_options.push_back( dv == ctx.int_val(variable) and not(ctx.int_val(state_valuation[variable]) > vv)); - } + if(state_valuation[variable] > 0) { + // not (Vi = vj => sj<=xj) + step_options_true.push_back( dv == ctx.int_val(variable) and not(ctx.int_val(state_valuation[variable]) <= vv)); + } + if(state_valuation[variable] < variable_domain[variable].size()-1) { + step_options_false.push_back( dv == ctx.int_val(variable) and not(ctx.int_val(state_valuation[variable]) > vv)); } } - substituted.push_back(z3::mk_or(step_options)); + this->substituted_true = z3::mk_or(step_options_true); + this->substituted_false = z3::mk_or(step_options_false); + child_true->createPrefixSubstitutions(state_valuation); + child_false->createPrefixSubstitutions(state_valuation); +} - getChild(step_to_true_child)->substitutePrefixExpression(path,state_valuation,substituted); +void InnerNode::substitutePrefixExpression(std::vector const& path, z3::expr_vector & substituted) const { + bool step_to_true_child = path[depth]; + substituted.push_back(step_to_true_child ? substituted_true : substituted_false); + getChild(step_to_true_child)->substitutePrefixExpression(path,substituted); } z3::expr InnerNode::substituteActionExpression(std::vector const& path, uint64_t action) const { return getChild(path[depth])->substituteActionExpression(path,action); } -void InnerNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const { +/*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); +}*/ + +void InnerNode::createPrefixSubstitutionsHarmonizing(z3::expr_vector const& state_valuation) { + this->substituted_true = step_true_harm.substitute(state_substitution_variables,state_valuation); + this->substituted_false = step_false_harm.substitute(state_substitution_variables,state_valuation); + child_true->createPrefixSubstitutionsHarmonizing(state_valuation); + child_false->createPrefixSubstitutionsHarmonizing(state_valuation); } +void InnerNode::substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector & substituted) const { + bool step_to_true_child = path[depth]; + substituted.push_back(step_to_true_child ? substituted_true : substituted_false); + getChild(step_to_true_child)->substitutePrefixExpressionHarmonizing(path,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); } diff --git a/payntbind/src/synthesis/quotient/TreeNode.h b/payntbind/src/synthesis/quotient/TreeNode.h index 9dc378fc..71860682 100644 --- a/payntbind/src/synthesis/quotient/TreeNode.h +++ b/payntbind/src/synthesis/quotient/TreeNode.h @@ -118,11 +118,14 @@ class TreeNode { virtual uint64_t getPathActionHole(std::vector const& path) {return 0;} /** Add a step expression evaluated for a given state valuation. */ - virtual void substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const {}; + virtual void createPrefixSubstitutions(std::vector const& state_valuation) {}; + virtual void substitutePrefixExpression(std::vector const& path, z3::expr_vector & substituted) const {}; /** Add an action expression evaluated for a given state valuation. */ virtual z3::expr substituteActionExpression(std::vector const& path, uint64_t action) const {return z3::expr(ctx);}; + /** Add a step expression evaluated for a given state valuation (harmonizing). */ - virtual void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {}; + virtual void createPrefixSubstitutionsHarmonizing(z3::expr_vector const& state_valuation) {}; + virtual void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector & substituted) const {}; /** Add an action expression evaluated for a given state valuation (harmonizing). */ virtual z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const {return z3::expr(ctx);}; @@ -175,9 +178,12 @@ class TerminalNode: public TreeNode { void createPaths(z3::expr const& harmonizing_variable) override; uint64_t getPathActionHole(std::vector const& path); - void substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const override; + void createPrefixSubstitutions(std::vector const& state_valuation) override; + void substitutePrefixExpression(std::vector const& path, z3::expr_vector & substituted) const override; z3::expr substituteActionExpression(std::vector const& path, uint64_t action) const override; - void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; + + void createPrefixSubstitutionsHarmonizing(z3::expr_vector const& state_valuation) override; + void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector & substituted) const override; z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const override; void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override; @@ -217,6 +223,9 @@ class InnerNode: public TreeNode { z3::expr step_true_harm; z3::expr step_false_harm; + z3::expr substituted_true; + z3::expr substituted_false; + InnerNode( uint64_t identifier, z3::context & ctx, std::vector const& variable_name, @@ -229,9 +238,12 @@ class InnerNode: public TreeNode { void createPaths(z3::expr const& harmonizing_variable) override; uint64_t getPathActionHole(std::vector const& path); - void substitutePrefixExpression(std::vector const& path, std::vector const& state_valuation, z3::expr_vector & substituted) const override; + void createPrefixSubstitutions(std::vector const& state_valuation) override; + void substitutePrefixExpression(std::vector const& path, z3::expr_vector & substituted) const override; z3::expr substituteActionExpression(std::vector const& path, uint64_t action) const override; - void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const override; + + void createPrefixSubstitutionsHarmonizing(z3::expr_vector const& state_valuation) override; + void substitutePrefixExpressionHarmonizing(std::vector const& path, z3::expr_vector & substituted) const override; z3::expr substituteActionExpressionHarmonizing(std::vector const& path, uint64_t action, z3::expr const& harmonizing_variable) const override; void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override;