mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-24 10:59:38 +00:00
Code Activity

remove unused function

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-23 13:03:58 -07:00
parent e045e650da
commit 1cf5e3e300
1 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq/seq_nielsen.h
View file

@ -740,10 +740,6 @@ namespace seq {
// true if all str_eqs are trivial and there are no str_mems // true if all str_eqs are trivial and there are no str_mems
bool is_satisfied() const; bool is_satisfied() const;
// true if any constraint has opaque (s_var) terms that
// the Nielsen graph cannot decompose
bool has_opaque_terms() const;
// render constraint set as an HTML fragment for DOT node labels. // render constraint set as an HTML fragment for DOT node labels.
// mirrors ZIPT's NielsenNode.ToHtmlString() // mirrors ZIPT's NielsenNode.ToHtmlString()
std::ostream& to_html(std::ostream& out, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m) const; std::ostream& to_html(std::ostream& out, obj_map<expr, std::string>& names, uint64_t& next_id, ast_manager& m) const;