Rename validate_bit_vector_predicate_arguments to validate_bit_vector_operator_arguments.

NlightNFotis · NlightNFotis · commit b11a3b2ae950 · 2022-02-03T12:00:24.000Z
This allows the name to reflect the more general purpose deployment of this function.
diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp
@@ -4,7 +4,7 @@
 
 #include <util/invariant.h>
 
-static void validate_bit_vector_predicate_arguments(
+static void validate_bit_vector_operator_arguments(
   const smt_termt &left,
   const smt_termt &right)
 {
@@ -37,7 +37,7 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -60,7 +60,7 @@ void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -83,7 +83,7 @@ void smt_bit_vector_theoryt::unsigned_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -107,7 +107,7 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -130,7 +130,7 @@ void smt_bit_vector_theoryt::signed_less_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -153,7 +153,7 @@ void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -176,7 +176,7 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -199,7 +199,7 @@ void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -222,7 +222,7 @@ void smt_bit_vector_theoryt::addt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::addt>
@@ -244,7 +244,7 @@ void smt_bit_vector_theoryt::subtractt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -267,7 +267,7 @@ void smt_bit_vector_theoryt::multiplyt::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -290,7 +290,7 @@ void smt_bit_vector_theoryt::unsigned_dividet::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -313,7 +313,7 @@ void smt_bit_vector_theoryt::signed_dividet::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -336,7 +336,7 @@ void smt_bit_vector_theoryt::unsigned_remaindert::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<
@@ -359,7 +359,7 @@ void smt_bit_vector_theoryt::signed_remaindert::validate(
   const smt_termt &lhs,
   const smt_termt &rhs)
 {
-  validate_bit_vector_predicate_arguments(lhs, rhs);
+  validate_bit_vector_operator_arguments(lhs, rhs);
 }
 
 const smt_function_application_termt::factoryt<

Original file line number	Diff line number	Diff line change
`@@ -4,7 +4,7 @@`
`4`	`4`
`5`	`5`	`#include <util/invariant.h>`
`6`	`6`
`7`		`-static void validate_bit_vector_predicate_arguments(`
	`7`	`+static void validate_bit_vector_operator_arguments(`
`8`	`8`	`const smt_termt &left,`
`9`	`9`	`const smt_termt &right)`
`10`	`10`	`{`
`@@ -37,7 +37,7 @@ void smt_bit_vector_theoryt::unsigned_less_thant::validate(`
`37`	`37`	`const smt_termt &lhs,`
`38`	`38`	`const smt_termt &rhs)`
`39`	`39`	`{`
`40`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`40`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`41`	`41`	`}`
`42`	`42`
`43`	`43`	`const smt_function_application_termt::factoryt<`
`@@ -60,7 +60,7 @@ void smt_bit_vector_theoryt::unsigned_less_than_or_equalt::validate(`
`60`	`60`	`const smt_termt &lhs,`
`61`	`61`	`const smt_termt &rhs)`
`62`	`62`	`{`
`63`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`63`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`64`	`64`	`}`
`65`	`65`
`66`	`66`	`const smt_function_application_termt::factoryt<`
`@@ -83,7 +83,7 @@ void smt_bit_vector_theoryt::unsigned_greater_thant::validate(`
`83`	`83`	`const smt_termt &lhs,`
`84`	`84`	`const smt_termt &rhs)`
`85`	`85`	`{`
`86`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`86`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`87`	`87`	`}`
`88`	`88`
`89`	`89`	`const smt_function_application_termt::factoryt<`
`@@ -107,7 +107,7 @@ void smt_bit_vector_theoryt::unsigned_greater_than_or_equalt::validate(`
`107`	`107`	`const smt_termt &lhs,`
`108`	`108`	`const smt_termt &rhs)`
`109`	`109`	`{`
`110`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`110`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`111`	`111`	`}`
`112`	`112`
`113`	`113`	`const smt_function_application_termt::factoryt<`
`@@ -130,7 +130,7 @@ void smt_bit_vector_theoryt::signed_less_thant::validate(`
`130`	`130`	`const smt_termt &lhs,`
`131`	`131`	`const smt_termt &rhs)`
`132`	`132`	`{`
`133`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`133`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`134`	`134`	`}`
`135`	`135`
`136`	`136`	`const smt_function_application_termt::factoryt<`
`@@ -153,7 +153,7 @@ void smt_bit_vector_theoryt::signed_less_than_or_equalt::validate(`
`153`	`153`	`const smt_termt &lhs,`
`154`	`154`	`const smt_termt &rhs)`
`155`	`155`	`{`
`156`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`156`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`157`	`157`	`}`
`158`	`158`
`159`	`159`	`const smt_function_application_termt::factoryt<`
`@@ -176,7 +176,7 @@ void smt_bit_vector_theoryt::signed_greater_thant::validate(`
`176`	`176`	`const smt_termt &lhs,`
`177`	`177`	`const smt_termt &rhs)`
`178`	`178`	`{`
`179`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`179`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`180`	`180`	`}`
`181`	`181`
`182`	`182`	`const smt_function_application_termt::factoryt<`
`@@ -199,7 +199,7 @@ void smt_bit_vector_theoryt::signed_greater_than_or_equalt::validate(`
`199`	`199`	`const smt_termt &lhs,`
`200`	`200`	`const smt_termt &rhs)`
`201`	`201`	`{`
`202`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`202`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`203`	`203`	`}`
`204`	`204`
`205`	`205`	`const smt_function_application_termt::factoryt<`
`@@ -222,7 +222,7 @@ void smt_bit_vector_theoryt::addt::validate(`
`222`	`222`	`const smt_termt &lhs,`
`223`	`223`	`const smt_termt &rhs)`
`224`	`224`	`{`
`225`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`225`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`226`	`226`	`}`
`227`	`227`
`228`	`228`	`const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::addt>`
`@@ -244,7 +244,7 @@ void smt_bit_vector_theoryt::subtractt::validate(`
`244`	`244`	`const smt_termt &lhs,`
`245`	`245`	`const smt_termt &rhs)`
`246`	`246`	`{`
`247`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`247`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`248`	`248`	`}`
`249`	`249`
`250`	`250`	`const smt_function_application_termt::factoryt<`
`@@ -267,7 +267,7 @@ void smt_bit_vector_theoryt::multiplyt::validate(`
`267`	`267`	`const smt_termt &lhs,`
`268`	`268`	`const smt_termt &rhs)`
`269`	`269`	`{`
`270`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`270`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`271`	`271`	`}`
`272`	`272`
`273`	`273`	`const smt_function_application_termt::factoryt<`
`@@ -290,7 +290,7 @@ void smt_bit_vector_theoryt::unsigned_dividet::validate(`
`290`	`290`	`const smt_termt &lhs,`
`291`	`291`	`const smt_termt &rhs)`
`292`	`292`	`{`
`293`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`293`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`294`	`294`	`}`
`295`	`295`
`296`	`296`	`const smt_function_application_termt::factoryt<`
`@@ -313,7 +313,7 @@ void smt_bit_vector_theoryt::signed_dividet::validate(`
`313`	`313`	`const smt_termt &lhs,`
`314`	`314`	`const smt_termt &rhs)`
`315`	`315`	`{`
`316`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`316`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`317`	`317`	`}`
`318`	`318`
`319`	`319`	`const smt_function_application_termt::factoryt<`
`@@ -336,7 +336,7 @@ void smt_bit_vector_theoryt::unsigned_remaindert::validate(`
`336`	`336`	`const smt_termt &lhs,`
`337`	`337`	`const smt_termt &rhs)`
`338`	`338`	`{`
`339`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`339`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`340`	`340`	`}`
`341`	`341`
`342`	`342`	`const smt_function_application_termt::factoryt<`
`@@ -359,7 +359,7 @@ void smt_bit_vector_theoryt::signed_remaindert::validate(`
`359`	`359`	`const smt_termt &lhs,`
`360`	`360`	`const smt_termt &rhs)`
`361`	`361`	`{`
`362`		`- validate_bit_vector_predicate_arguments(lhs, rhs);`
	`362`	`+ validate_bit_vector_operator_arguments(lhs, rhs);`
`363`	`363`	`}`
`364`	`364`
`365`	`365`	`const smt_function_application_termt::factoryt<`