diff --git a/plugins/bitwuzla_utils/include/bitwuzla_utils/bitwuzla_utils.h b/plugins/bitwuzla_utils/include/bitwuzla_utils/bitwuzla_utils.h index 96fe9080a8a..28668ff9ff3 100644 --- a/plugins/bitwuzla_utils/include/bitwuzla_utils/bitwuzla_utils.h +++ b/plugins/bitwuzla_utils/include/bitwuzla_utils/bitwuzla_utils.h @@ -84,6 +84,15 @@ namespace hal */ std::set get_variable_names(const bitwuzla::Term& t); + + /** + * Extracts all variables as term from a bitwuzla term. + * + * @param[in] t - The term to extract the variable names from. + * @returns A vectir containing all the variables + */ + Result> get_variables(const bitwuzla::Term& t); + /** * Extracts all net ids from the variables of a bitwuzla term. * @@ -134,9 +143,34 @@ namespace hal * @return The the bitwuzla term representations of combined Boolean functions of the subgraph on success, an error otherwise. */ Result> get_subgraph_bitwuzla_functions(const std::vector& subgraph_gates, const std::vector& subgraph_outputs); - + /** + * Simplify the provided Term with optional replacements as much as possible + * + * @param[in] t - The term to simplify. + * @param[in] id_to_term - Terms with the given ids will be replaced with Terms specified in the map. + * @return The simplified version of the term t. + */ Result simplify(const bitwuzla::Term& t); Result simplify(const bitwuzla::Term& t, std::map& id_to_term); + /** + * Evalute the provided Term when a value is given for each variable. + * + * @param[in] t - The term to evaluate. + * @param[in] id_to_value - A map of each variable mapped to a constant value which will be evaluated. This will fail if the value does not fit into size of the given Variable. + * @return The evaluated version of the term t as Constant. + */ + + Result evaluate(const bitwuzla::Term& t,std::map& id_to_value); + + /** + * Substitue Subterms of the provided Term with other terms and simplify afterwards. + * + * @param[in] t - The term to evaluate. + * @param[in] term_to_term - A map of Terms with the corresponding Terms to replace them with. + * @return The substituted version of the term t. + */ + Result substitue(const bitwuzla::Term& t,std::map< u64,bitwuzla::Term>& id_to_term); + } // namespace bitwuzla_utils } // namespace hal diff --git a/plugins/bitwuzla_utils/include/bitwuzla_utils/symbolic_execution.h b/plugins/bitwuzla_utils/include/bitwuzla_utils/symbolic_execution.h index f5181d5b193..9c3bafef1c7 100644 --- a/plugins/bitwuzla_utils/include/bitwuzla_utils/symbolic_execution.h +++ b/plugins/bitwuzla_utils/include/bitwuzla_utils/symbolic_execution.h @@ -43,7 +43,7 @@ namespace hal * @param[in] function - The Boolean function to evaluate. * @returns Ok() and the evaluated Boolean function on success, Err() otherwise. */ - Result evaluate(const bitwuzla::Term& function, std::map id_to_term) const; + Result evaluate(const bitwuzla::Term& function, std::map id_to_term,std::map& resulting_id_to_term) const; // /** // * Evaluates an equality constraint and applies it to the symbolic state of the symbolic execution. diff --git a/plugins/bitwuzla_utils/src/bitwuzla_utils.cpp b/plugins/bitwuzla_utils/src/bitwuzla_utils.cpp index f8333b1c5e3..ed1a080428a 100644 --- a/plugins/bitwuzla_utils/src/bitwuzla_utils.cpp +++ b/plugins/bitwuzla_utils/src/bitwuzla_utils.cpp @@ -468,24 +468,137 @@ namespace hal { bitwuzla::Term current = t; bitwuzla::Term before; + std::map resulting_id_to_term; do { before = current; - auto simplified = SMT::SymbolicExecution().evaluate(current, id_to_term); + auto simplified = SMT::SymbolicExecution().evaluate(current, id_to_term,resulting_id_to_term); if (simplified.is_error()) { return ERR_APPEND(simplified.get_error(), "could not apply local simplification: symbolic execution failed"); } current = simplified.get(); } while (before != current); - // auto simplified = SMT::SymbolicExecution().evaluate(current, id_to_term); - // if (simplified.is_error()) - // { - // return ERR_APPEND(simplified.get_error(), "could not apply local simplification: symbolic execution failed"); - // } - // return simplified; + id_to_term =resulting_id_to_term; return OK(current); } + //actual returns Terms inside a Term for each variable + // way slower than SMT string but this way IDs can be used + Result> get_variables(const bitwuzla::Term& t) + { + // + std::vector result; + if (t.num_children() > 0) + { + auto children = t.children(); + for (const auto cur_child : children) + { + auto child_res = get_variables(cur_child).get(); + for(auto cur_child: child_res) + { + bool doubled = false; + for(auto term: result) + { + if(term.id() == t.id()) + { + doubled = true; + break; + } + } + if(!doubled) + { + result.push_back(t); + } + } + } + } + else + { + if(t.is_variable()) + { + bool doubled = false; + for(auto term: result) + { + if(term.id() == t.id()) + { + doubled = true; + break; + } + } + if(!doubled) + { + result.push_back(t); + } + + } + } + return OK(result); + } + Result substitue(const bitwuzla::Term& t,std::map< u64,bitwuzla::Term>& id_to_term) + { + + std::map res; + auto simplified = SMT::SymbolicExecution().evaluate(t,id_to_term ,res); + if (simplified.is_error()) + { + return ERR_APPEND(simplified.get_error(), "could not apply local substitution: symbolic execution failed"); + } + return simplified; + } + Result evaluate(const bitwuzla::Term& t,std::map& id_to_value) + { + auto variables = get_variables(t); + + std::map< u64,bitwuzla::Term> id_to_initial_term; + if(variables.is_error()) + { + return ERR("Could not resolve variables of given Term."); + } + if(variables.get().size() != id_to_value.size()) + { + return ERR("Variables given are not the same amount as expected."); + } + for(auto current_var: variables.get()) + { + if(id_to_value.find(current_var.id()) == id_to_value.end()) + { + return ERR("Did not specify value for variable "+current_var.str()); + } + else{ + id_to_initial_term[current_var.id()] =current_var; + } + } + + std::map< u64,bitwuzla::Term> id_to_term; + for(auto [id,value] :id_to_value) + { + u64 arity = id_to_initial_term[id].sort().bv_size(); + if((value >> arity)!= 0) + { + return ERR("The given value for variable " + id_to_initial_term[id].str() + " does not fit into the size of that variable."); + } + id_to_term[id] =bitwuzla::mk_bv_value_uint64(bitwuzla::mk_bv_sort(arity), value); + } + + bitwuzla::Term current = t; + bitwuzla::Term before; + do + { + before = current; + std::map res; + auto simplified = SMT::SymbolicExecution().evaluate(current, id_to_term,res); + if (simplified.is_error()) + { + return ERR_APPEND(simplified.get_error(), "could not apply constant propagation: symbolic execution failed"); + } + current = simplified.get(); + } while (before != current); + if(current.is_const()) + { + return OK(current); + } + return ERR("Could not resolve inputs to constant value."); + } } // namespace bitwuzla_utils } // namespace hal diff --git a/plugins/bitwuzla_utils/src/symbolic_execution.cpp b/plugins/bitwuzla_utils/src/symbolic_execution.cpp index 38f7371ab72..18fb6082398 100644 --- a/plugins/bitwuzla_utils/src/symbolic_execution.cpp +++ b/plugins/bitwuzla_utils/src/symbolic_execution.cpp @@ -507,6 +507,10 @@ namespace hal std::vector get_terms_dfs(const bitwuzla::Term& function, std::map& id_to_term) { std::vector result; + if(id_to_term.find(function.id()) != id_to_term.end()) + { + return result; + } if (function.num_children() > 0) { auto children = function.children(); @@ -528,7 +532,7 @@ namespace hal } } // namespace - Result SymbolicExecution::evaluate(const bitwuzla::Term& function, std::map id_to_term) const + Result SymbolicExecution::evaluate(const bitwuzla::Term& function, std::map id_to_term,std::map& resulting_id_to_term) const { //std::map id_to_term; std::vector stack = get_terms_dfs(function, id_to_term); @@ -567,7 +571,7 @@ namespace hal } } - + resulting_id_to_term = id_to_term; return OK(result); } diff --git a/plugins/bitwuzla_utils/test/bitwuzla_simplification.cpp b/plugins/bitwuzla_utils/test/bitwuzla_simplification.cpp index 14e555b08ae..41faf9f6ff2 100644 --- a/plugins/bitwuzla_utils/test/bitwuzla_simplification.cpp +++ b/plugins/bitwuzla_utils/test/bitwuzla_simplification.cpp @@ -822,14 +822,31 @@ namespace hal "I1)) & I2) & I3) & I4) & I5)) | (((((I0 & (! I1)) & I2) & I3) & I4) & I5)) | (((((I0 & I1) & I2) & I3) & I4) & I5))") .get(); auto bf_function = bitwuzla_utils::from_bf(function).get(); + + std::map res; auto start = std::chrono::system_clock::now(); - const auto simplified = bitwuzla_utils::simplify(bf_function); + const auto simplified = bitwuzla_utils::simplify(bf_function,res); const auto duration_in_seconds = std::chrono::duration(std::chrono::system_clock::now() - start).count(); + + for(auto [id,term]:res) + { + std::cout << id << ":" << term.str() <(std::chrono::system_clock::now() - start).count(); + + + + start = std::chrono::system_clock::now(); const auto bf_simplified = function.simplify(); const auto bf_duration_in_seconds = std::chrono::duration(std::chrono::system_clock::now() - start).count(); std::cout << "BW_simplification took "<< duration_in_seconds<< " seconds"<< std::endl; + std::cout << "BW_simplification took "<< duration_in_seconds_second_time<< " seconds the second time"<< std::endl; std::cout << "BF_simplification took "<< bf_duration_in_seconds<< " seconds"<< std::endl; }