mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

remove commented-out old worklists

Browse source
This commit is contained in:
Murphy Berzish 2017-02-14 18:45:09 -05:00
parent d5b1e4b015
commit f9b3c47bf5
1 changed files with 1 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_str.h
View file

@ -209,20 +209,7 @@ namespace smt {
ptr_vector<enode> m_string_constant_length_todo;
ptr_vector<enode> m_concat_eval_todo;
// enode lists for term-specific axioms
/*
ptr_vector<enode> m_axiom_CharAt_todo;
ptr_vector<enode> m_axiom_StartsWith_todo;
ptr_vector<enode> m_axiom_EndsWith_todo;
ptr_vector<enode> m_axiom_Contains_todo;
ptr_vector<enode> m_axiom_Indexof_todo;
ptr_vector<enode> m_axiom_Indexof2_todo;
ptr_vector<enode> m_axiom_LastIndexof_todo;
ptr_vector<enode> m_axiom_Substr_todo;
ptr_vector<enode> m_axiom_Replace_todo;
ptr_vector<enode> m_axiom_RegexIn_todo;
*/
// enode lists for library-aware/high-level string terms (e.g. substr, contains)
ptr_vector<enode> m_library_aware_axiom_todo;
// hashtable of all exprs for which we've already set up term-specific axioms --