Skip to content

Commit

Permalink
faster path formula creation
Browse files Browse the repository at this point in the history
  • Loading branch information
Roman Andriushchenko committed Oct 3, 2024
1 parent 9a81712 commit efcc202
Show file tree
Hide file tree
Showing 4 changed files with 73 additions and 37 deletions.
15 changes: 8 additions & 7 deletions payntbind/src/synthesis/quotient/ColoringSmt.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,20 +137,20 @@ ColoringSmt<ValueType>::ColoringSmt(

std::vector<z3::expr_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<z3::expr_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);
}
}

Expand All @@ -173,10 +173,11 @@ ColoringSmt<ValueType>::ColoringSmt(
timers["ColoringSmt:: create harmonizing variants"].start();
std::vector<z3::expr_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));
}
}
Expand Down
6 changes: 3 additions & 3 deletions payntbind/src/synthesis/quotient/ColoringSmt.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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. */
Expand Down Expand Up @@ -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;

};

}
65 changes: 44 additions & 21 deletions payntbind/src/synthesis/quotient/TreeNode.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -164,16 +164,23 @@ uint64_t TerminalNode::getPathActionHole(std::vector<bool> const& path) {
return action_hole.hole;
}

void TerminalNode::createPrefixSubstitutions(std::vector<uint64_t> const& state_valuation) {
//
}

void TerminalNode::substitutePrefixExpression(std::vector<bool> const& path, std::vector<uint64_t> const& state_valuation, z3::expr_vector & substituted) const {
void TerminalNode::substitutePrefixExpression(std::vector<bool> const& path, z3::expr_vector & substituted) const {
//
}

z3::expr TerminalNode::substituteActionExpression(std::vector<bool> const& path, uint64_t action) const {
return action_hole.solver_variable == (int)action;
}

void TerminalNode::substitutePrefixExpressionHarmonizing(std::vector<bool> 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<bool> const& path, z3::expr_vector & substituted) const {
//
}

Expand Down Expand Up @@ -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());
Expand Down Expand Up @@ -374,43 +381,59 @@ uint64_t InnerNode::getPathActionHole(std::vector<bool> const& path) {
}


void InnerNode::substitutePrefixExpression(std::vector<bool> const& path, std::vector<uint64_t> 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<uint64_t> 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<bool> 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<bool> const& path, uint64_t action) const {
return getChild(path[depth])->substituteActionExpression(path,action);
}

void InnerNode::substitutePrefixExpressionHarmonizing(std::vector<bool> const& path, z3::expr_vector const& state_valuation, z3::expr_vector & substituted) const {
/*void InnerNode::substitutePrefixExpressionHarmonizing(std::vector<bool> 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<bool> 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<bool> const& path, uint64_t action, z3::expr const& harmonizing_variable) const {
return getChild(path[depth])->substituteActionExpressionHarmonizing(path,action,harmonizing_variable);
}
Expand Down
24 changes: 18 additions & 6 deletions payntbind/src/synthesis/quotient/TreeNode.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -118,11 +118,14 @@ class TreeNode {
virtual uint64_t getPathActionHole(std::vector<bool> const& path) {return 0;}

/** Add a step expression evaluated for a given state valuation. */
virtual void substitutePrefixExpression(std::vector<bool> const& path, std::vector<uint64_t> const& state_valuation, z3::expr_vector & substituted) const {};
virtual void createPrefixSubstitutions(std::vector<uint64_t> const& state_valuation) {};
virtual void substitutePrefixExpression(std::vector<bool> const& path, z3::expr_vector & substituted) const {};
/** Add an action expression evaluated for a given state valuation. */
virtual z3::expr substituteActionExpression(std::vector<bool> 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<bool> 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<bool> const& path, z3::expr_vector & substituted) const {};
/** Add an action expression evaluated for a given state valuation (harmonizing). */
virtual z3::expr substituteActionExpressionHarmonizing(std::vector<bool> const& path, uint64_t action, z3::expr const& harmonizing_variable) const {return z3::expr(ctx);};

Expand Down Expand Up @@ -175,9 +178,12 @@ class TerminalNode: public TreeNode {
void createPaths(z3::expr const& harmonizing_variable) override;
uint64_t getPathActionHole(std::vector<bool> const& path);

void substitutePrefixExpression(std::vector<bool> const& path, std::vector<uint64_t> const& state_valuation, z3::expr_vector & substituted) const override;
void createPrefixSubstitutions(std::vector<uint64_t> const& state_valuation) override;
void substitutePrefixExpression(std::vector<bool> const& path, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpression(std::vector<bool> const& path, uint64_t action) const override;
void substitutePrefixExpressionHarmonizing(std::vector<bool> 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<bool> const& path, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpressionHarmonizing(std::vector<bool> const& path, uint64_t action, z3::expr const& harmonizing_variable) const override;

void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override;
Expand Down Expand Up @@ -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<std::string> const& variable_name,
Expand All @@ -229,9 +238,12 @@ class InnerNode: public TreeNode {
void createPaths(z3::expr const& harmonizing_variable) override;
uint64_t getPathActionHole(std::vector<bool> const& path);

void substitutePrefixExpression(std::vector<bool> const& path, std::vector<uint64_t> const& state_valuation, z3::expr_vector & substituted) const override;
void createPrefixSubstitutions(std::vector<uint64_t> const& state_valuation) override;
void substitutePrefixExpression(std::vector<bool> const& path, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpression(std::vector<bool> const& path, uint64_t action) const override;
void substitutePrefixExpressionHarmonizing(std::vector<bool> 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<bool> const& path, z3::expr_vector & substituted) const override;
z3::expr substituteActionExpressionHarmonizing(std::vector<bool> const& path, uint64_t action, z3::expr const& harmonizing_variable) const override;

void addFamilyEncoding(Family const& subfamily, z3::solver & solver) const override;
Expand Down

0 comments on commit efcc202

Please sign in to comment.