add evaluate and subsitute utilizing preexisting functions

plugins/bitwuzla_utils/include/bitwuzla_utils/bitwuzla_utils.h

@@ -84,6 +84,15 @@ namespace hal
          */
         std::set<std::string> 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<std::vector<bitwuzla::Term>> 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<std::vector<bitwuzla::Term>> get_subgraph_bitwuzla_functions(const std::vector<Gate*>& subgraph_gates, const std::vector<Net*>& 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<bitwuzla::Term> simplify(const bitwuzla::Term& t);
         Result<bitwuzla::Term> simplify(const bitwuzla::Term& t, std::map<u64, bitwuzla::Term>& 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<bitwuzla::Term> evaluate(const bitwuzla::Term& t,std::map<u64,u64>& 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<bitwuzla::Term> substitue(const bitwuzla::Term& t,std::map< u64,bitwuzla::Term>& id_to_term);
+
     }    // namespace bitwuzla_utils
 }    // namespace hal

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<bitwuzla::Term> evaluate(const bitwuzla::Term& function, std::map<u64, bitwuzla::Term> id_to_term) const;
+            Result<bitwuzla::Term> evaluate(const bitwuzla::Term& function, std::map<u64, bitwuzla::Term> id_to_term,std::map<u64, bitwuzla::Term>& resulting_id_to_term) const;
 
             // /**
             //  * Evaluates an equality constraint and applies it to the symbolic state of the symbolic execution.

plugins/bitwuzla_utils/src/bitwuzla_utils.cpp

@@ -468,24 +468,137 @@ namespace hal
         {
             bitwuzla::Term current = t;
             bitwuzla::Term before;
+            std::map<u64, bitwuzla::Term> 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<std::vector<bitwuzla::Term>> get_variables(const bitwuzla::Term& t)
+        {
+            //
+            std::vector<bitwuzla::Term> 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<bitwuzla::Term> substitue(const bitwuzla::Term& t,std::map< u64,bitwuzla::Term>& id_to_term)
+        {
+
+            std::map<u64, bitwuzla::Term> 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<bitwuzla::Term> evaluate(const bitwuzla::Term& t,std::map<u64,u64>& 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<u64, bitwuzla::Term> 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

plugins/bitwuzla_utils/src/symbolic_execution.cpp

@@ -507,6 +507,10 @@ namespace hal
             std::vector<bitwuzla::Term> get_terms_dfs(const bitwuzla::Term& function, std::map<u64, bitwuzla::Term>& id_to_term)
             {
                 std::vector<bitwuzla::Term> 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<bitwuzla::Term> SymbolicExecution::evaluate(const bitwuzla::Term& function, std::map<u64, bitwuzla::Term> id_to_term) const
+        Result<bitwuzla::Term> SymbolicExecution::evaluate(const bitwuzla::Term& function, std::map<u64, bitwuzla::Term> id_to_term,std::map<u64, bitwuzla::Term>& resulting_id_to_term) const
         {
             //std::map<u64, bitwuzla::Term> id_to_term;
             std::vector<bitwuzla::Term> stack = get_terms_dfs(function, id_to_term);
@@ -567,7 +571,7 @@ namespace hal
 
                 }
             }
-
+            resulting_id_to_term = id_to_term;
             return OK(result);
         }
 

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<u64, bitwuzla::Term> 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<double>(std::chrono::system_clock::now() - start).count();
+
+        for(auto [id,term]:res)
+        {
+            std::cout << id << ":" << term.str() <<std::endl;
+        }
+
+        start      = std::chrono::system_clock::now();
+        const auto simplified2 = bitwuzla_utils::simplify(bf_function,res);
+
+        const auto duration_in_seconds_second_time = std::chrono::duration<double>(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<double>(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;
     }